[isabelle-dev] Deglobalizing HOL.thy

[Lawrence Paulson]

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?
Larry

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
> showstopper!?
> 
> 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).