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.
berghofe [Wed, 07 May 2008 10:56:34 +0200] rev 26792
- Deleted code setup for finite and card
- Deleted proof of "instance set :: (finite) finite" and modified proof of
"instance fun :: (finite, finite) finite", which now uses some ideas from
the instance proof for sets
- Instantiated arg_cong rule to avoid problems with HO unification
berghofe [Wed, 07 May 2008 10:56:33 +0200] rev 26791
Instantiated subst rule to avoid problems with HO unification.
wenzelm [Tue, 06 May 2008 23:33:05 +0200] rev 26790
converted "General logic setup";
wenzelm [Tue, 06 May 2008 00:13:01 +0200] rev 26789
misc fixes and tuning;
wenzelm [Tue, 06 May 2008 00:12:03 +0200] rev 26788
updated generated file;
wenzelm [Tue, 06 May 2008 00:10:59 +0200] rev 26787
proper scoping of railaliases;
wenzelm [Tue, 06 May 2008 00:10:23 +0200] rev 26786
moved some railaliases here -- for proper scoping;
wenzelm [Tue, 06 May 2008 00:08:52 +0200] rev 26785
element: isakeyword markup;