HOL Constant Definitions Done Right
Author: Rob Arthan
Paper Information
| Title: | HOL Constant Definitions Done Right |
| Authors: | Rob Arthan |
| Proceedings: | ITP 2014 LNCS Proceedings |
| Editors: | Gerwin Klein and Ruben Gamboa |
| Keywords: | HOL, Conservative Extension, Constant Definition, Implicit Definition |
| Abstract: | ABSTRACT. This note gives a proposal for a simpler and more powerful replacement for the mechanisms currently provided in the various HOL implementation for defining new constants. |
| Pages: | 6 |
| Talk: | Jul 15 12:45 |
| Paper: |  |