Re: [isabelle] code generation for saturated naturals



Hi Peter,

>> Well, the first one(s) did not really perform well, but it was not very
>> difficult to get along without it.
> 
> What do you mean by "the first one(s)"? Lemmas, sledgehammers, ... ?

Well, the first metis class was very slow, I did not check the others
explicitly.

>> instantiation sat :: (len) complete_lattice
> 
> You've lost me here - the final instantiation in the theory is precisely this one.

This was a slip, it should read

instantiation sat :: (len) complete_distrib_lattice

which is still left as an exercise to prove.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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