[isabelle-dev] Deglobalizing HOL.thy

[Gerwin Klein]

Hi Florian,

as always, it will hurt a bit I guess, but I think it is the right thing to do.

Cheers,
Gerwin

On 19/08/2010, at 11:18 AM, Florian Haftmann wrote:

> Hi all,
> 
> with authentic syntax being default and thanks to antiquotations, we
> have now reached a state where we could replace all the remaining
> unqualified symbol names in HOL.thy (between "global" and "local").
> While this should be technically quite easy, there remain two open
> questions before proceeding.
> 
> 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).
> 
>    Florian
> 
> -- 
> 
> Home:
> http://www.in.tum.de/~haftmann
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev