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



Thanks!

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

cheers

chris

On 10/26/2012 04:19 PM, Andreas Lochbihler wrote:
Hi Christian,

the website still has the theory files.

http://isabelle.in.tum.de/nominal/activities/tphols09/idw.html

Andreas

Am 26.10.2012 08:59, schrieb Christian Sternagel:
What I found quite interesting was the presentation by Stefan Berghofer
of Isabelle conversions at the 2009 isabelle-dev workshop at Munich. He
first showed how to make a simplifier with a few conversions and
conversion combinators, then showed how to make it a little faster using
a "Boultonized" version of the same (like "Q" conversions in HOL), and
then showed how to make it really fast using the Isabelle Simplifier
techniques that came after conversions so many years ago.
Does anybody know whether slides/thy-files of this talk are still
around? (I did
not manage to find a website for any of the Isabelle Users Workshops
besides
2012.) - cheers chris








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