[isabelle-dev] Deglobalizing HOL.thy

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100819/3ff01e70/attachment.sig>