Re: [isabelle] Automatic derivation of a total order on datatypes

Am 14.11.2012 10:42, schrieb René Thiemann:
> Dear René
> as Andreas already stated, there is such an order generator in the AFP. 
> However, the tactics in the AFP-Entry for the Isabelle2012 release version 
> contain some known gaps, so that the generator may fail on some datatypes.
> All known gaps have been fixed in the development version of the AFP. 
> So, if you are working with the development version of Isabelle, just use the development version of the AFP.
> If however, you are working with Isabelle2012, then please download a fixed version of the AFP-entry at
> which contains all the fixes of the order generator and works with Isabelle2012.
> Best regards,
> René

Thanks for that. I didn't think of looking into the AFP to solve my

I'm now using the version of the .tgz above and it works \o/.

Is it somehow possible, though, to disable the trace output? There are
thousands of (debug?) lines spit into the trace window whenever I use a
"derive linorder foo"...

- René
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

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