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
> 
> http://cl-informatik.uibk.ac.at/software/ceta/Datatype_Order_Generator.tgz
> 
> 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
problem:).

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.