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



I do not have the slides of this talk it seems, but 
the theory Stefan presented in 2009 is here:

http://isabelle.in.tum.de/nominal/activities/tphols09/IDW/Conversions.thy

The workshops in 2009 and 2010 have their webpage here:

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

Christian

On Friday, October 26, 2012 at 15:59:47 (+0900), Christian Sternagel wrote:
 > > 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.