berghofe [Wed, 07 May 2008 10:56:37 +0200] rev 26795
- Explicitely applied predicate1I in a few proofs, because it is no longer
part of the claset
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
to_set attribute, because it is no longer applied automatically
berghofe [Wed, 07 May 2008 10:56:36 +0200] rev 26794
- Now imports Fun rather than Orderings
- Moved "Set as lattice" section behind "Fun as lattice" section, since
sets are just functions.
- The instantiations
instantiation set :: (type) distrib_lattice
instantiation set :: (type) complete_lattice
are no longer needed, and the former definitions inf_set_eq, sup_set_eq,
Inf_set_def, and Sup_set_def can now be derived from abstract properties
of sup, inf, etc.
berghofe [Wed, 07 May 2008 10:56:35 +0200] rev 26793
Instantiated some rules to avoid problems with HO unification.