[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 31 13:54:43 CEST 2017
>>> Concerning \mu and \nu, I am currently investigating whether an import
>>> swap could re-establish the situation known from Isabelle2016-1
>> see http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1
> I had overlooked that \mu and \nu are global constants when importing
> this material, which I had received from Simon Foster. This needs to be
> addressed properly.
I did have a look at the overall situation but IMHO there are too many
open ends which cannot be resolved before the upcoming release:
* »no_notation« would mess up the material considerably and is difficult
to place: traditionally, HOL-Algebra has no universal entry point which
is guaranteed to be imported after all other theories.
* Specific syntax could be placed into bundles, but this cannot be done
* Giving up \mu and \nu and coming up with an alternative syntax.
Each of these requires subtantial thinking and appears much too invasive
> Your workaround merely helps users of Group, not of Complete_Lattice.
That is the relevant point for the upcoming release: users of Group in
Isabelle2016-1 (and there are many, since Group is used in substantial
parts of both distribution of AFP) need not to worry about additional
syntactic artefacts in Isabelle2017 either; Complete_Lattice is new in
Isabelle2017 and does not induce any regression problems.
> Moreover, it doesn't make sense that Complete_Lattice imports Group, and
> that the structure theorem about subgroups is now in lattice theory.
The theorem in question requires both the notion of subgroup and
complete lattices, hence the import order dictates in which theory the
theorem has to reside (btw. the current import order is similar to
HOL-Main where Complete_Lattices comes after Groups). When placing it,
I followed the pre-existing textual reference
(http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1#l1.16). I am
happy to add the symmetric textual reference to Group.thy if this
clarifies the situation.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev