Michael Norrish
Michael Norrish
Closing with claim that `EVALn` is as good as it’s going to get.
Thanks for all your work on this!
To make this work you need to explicitly pass what Isabelle would call the proof context to the tactic that solves the goal. In HOL, this context would include (at...
- Amjad theorems don’t require a kernel change. - The contexts are a dynamic thing; I don’t see how PolyML namespaces would help
If there are type variables in the goal (quite plausibly), the constant standing in for the game will need to take type variable parameters (most easily using the `itself` type),...
A comment from Rob Arthan on the `hol-info` mailing list points out that one disadvantage of the HOL Light approach is that you will get ``` `{ x | x...
Of course, one shouldn't be use `=` on terms anyway. One would still have ``` aconv ``{x | x > 6}`` ``{x | x > 6}`` ``` in a possible...
Another argument in favour of this idea is that it seems impossible to make a congruence rule for `GSPEC` as we have it, but the congruence rule for HOL Light's...
As the `gmane` link has died, here is a brief description of the HOL Light approach. There's a `GSPEC` constant outermost that is a signal to the printer (like our...
The Sourceforge archive has some/all of this stored. [This link](https://sourceforge.net/p/hol/mailman/hol-info/thread/[email protected]/) seems to work at the moment (2024).