[isabelle-dev] Deglobalizing HOL.thy
lp15 at cam.ac.uk
Thu Aug 19 13:09:17 CEST 2010
Your proposal makes sense to me. Naturally it should be announced on the mailing list so that our users have ample warning.
One thing I don't get: if HOL.eq is already taken, why not map the equality symbol to something else?
On 19 Aug 2010, at 11:18, Florian Haftmann wrote:
> a) Applications outside there.
> The changes produced when introducing antiquotations for those critical
> constant symbols where quite tiny: 50 files in Isabelle (cs.
> d0385f2764d8) plus 3 files in the AFP (cs. 2d2437cc82b2), which is
> really not much taking into account the pervasiveness of expressions
> like Const ("op =", ...) etc. This should indicate that the
> dequalification does not produce major discrepancies in applications
> outside there, but perhaps some of you has knowledge about some
> b) Infix operators.
> Some unnamed have top be given proper names. My suggestions:
> op & ~> HOL.and
> op | ~> HOL.or
> op --> ~> HOL.implies
> op = HOL.eq
> The last suggests a renaming of the code-generation class operation
> HOL.eq to HOL.equals (which should not be a problem).
More information about the isabelle-dev