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
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"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and