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



Am 14.11.2012 16:55, schrieb René Thiemann:
>> 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"...
> 
> Tracing is now disabled, both in the AFP development version and in the .tgz-version 
> for Isabelle2012. You can download the new file at the same URL:

Thanks :). Is it (btw) intended that the generated hashfunctions are not
automatically marked as code-equations? At the moment I do:

derive hashable com
lemmas[code] = hashcode_com_def bounded_hashcode_com_def
def_hashmap_size_com_def

- 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.