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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
