Re: [isabelle] Eisbach documentation
On 14/03/18 12:22, Christian Sternagel wrote:
> 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
> The reason I mention this is the following stackoverflow question:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and