Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue



On Fri, 26 Oct 2012, Christian Sternagel wrote:

No wonder that searching for "Isabelle Users Workshop" did not give the desired result ;)... I forgot that in 2009 it was a "Developers Workshop".

De-facto it was an Isabelle/ML users workshop, with a little bit of outlook towards Isabelle/Scala (but in 2009 the latter was still very thin). Maybe we should make some "Isabelle proof development workshop" next time.

Anyway, I've just returned from one that was very interesting: mostly French Coq users learning about HOL specifications and Isar proofs. See also http://www.lri.fr/~wenzel/Isabelle_Orleans_2012/ and feel free to re-use material you might want for your own courses next time.


	Makarius





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