[isabelle-dev] Deglobalizing HOL.thy
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 19 12:18:51 CEST 2010
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
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).
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev