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:
> 
> https://stackoverflow.com/questions/49275588/isabelle-2017-support-for-proof-method-definitons-seems-to-be-lacking

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.