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
> eisbach").
> 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 MHonArc.