Re: [isabelle] Problem with unfolding definitions while instantiating class



> This is not possible. As Dave pointed out, the problem goes away if in Main the
> instantiation of "fun" on class complete_lattice is done in stages, where in a
> first step one merely instantiates Sup and Inf.
> 
> @ Florian: any objections to that?

No.  This would finally conclude the »syntactification« of Sup and Inf
initiated by Larry (AFAIR).

	Florian

-- 

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.