Email Gateway (Aug 22 2022 at 16:56): Email Gateway (Aug 22 2022 at 16:56):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Eisbachers,
it might be a good idea to mention how to set up a theory file for using
Eisbach (at least I didn't spot a corresponding hint in "isabelle doc
eisbach").
The reason I mention this is the following stackoverflow question:
cheers
chris
Email Gateway (Aug 22 2022 at 16:57):From: Makarius <makarius@sketis.net>
Thanks for pointing this out.
Note that imports via file-names from other sessions are obsolete and
can lead into strange situations: instead of
"~~/src/HOL/Eisbach/Eisbach" it should be "HOL-Eisbach.Eisbach"
This also reminds me that Eisbach still needs to be reorganized
slightly, to make it work smoothly with Pure -- the problem is the
divergent clone of the "of" attribute.
Makarius
Last updated: Apr 26 2024 at 08:19 UTC