"Sup" is now a parameter for class complete_lattice rather than a
derived definition. INCOMPATIBILITY. Instantation of class
complete_lattice requires explicit definition for "Sup". Corresponding
theorem renames:
Sup_def ~> Sup_Inf
Sup_bool_eq ~> Sup_bool_def
Sup_set_eq ~> Sup_set_def
Sup_fun_eq ~> Sup_fun_def
Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 249 bytes
Desc: OpenPGP digital signature
Url :
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20070820/49ed046f/attachment.pgp
