[isabelle-dev] Deglobalizing HOL.thy
kleing at cse.unsw.edu.au
Thu Aug 19 12:38:04 CEST 2010
as always, it will hurt a bit I guess, but I think it is the right thing to do.
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
> 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).
> PGP available:
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev