[isabelle-dev] NEWS

[Florian Haftmann]

"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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20070820/49ed046f/attachment.sig>