Wed, 07 May 2008 10:56:41 +0200 Deleted instance "set :: (type) power" and moved instance
berghofe [Wed, 07 May 2008 10:56:41 +0200] rev 26799
Deleted instance "set :: (type) power" and moved instance "fun :: (type, type) power" to the beginning of the theory
Wed, 07 May 2008 10:56:40 +0200 split_beta is now declared as monotonicity rule, to allow bounded
berghofe [Wed, 07 May 2008 10:56:40 +0200] rev 26798
split_beta is now declared as monotonicity rule, to allow bounded quantifiers in introduction rules of inductive predicates.
Wed, 07 May 2008 10:56:39 +0200 - Added mem_def and predicate1I in some of the proofs
berghofe [Wed, 07 May 2008 10:56:39 +0200] rev 26797
- Added mem_def and predicate1I in some of the proofs - pred_equals_eq and pred_subset_eq are no longer used in the conversion between sets and predicates, because sets and predicates can no longer be distinguished
Wed, 07 May 2008 10:56:38 +0200 - Now imports Code_Setup, rather than Set and Fun, since the theorems
berghofe [Wed, 07 May 2008 10:56:38 +0200] rev 26796
- Now imports Code_Setup, rather than Set and Fun, since the theorems about orderings are already needed in Set - Moved "Dense orders" section to Set, since it requires set notation. - The "Order on sets" section is no longer necessary, since it is subsumed by the order on functions and booleans. - Moved proofs of Least_mono and Least_equality to Set, since they require set notation. - In proof of "instance fun :: (type, order) order", use ext instead of expand_fun_eq, since the latter is not yet available. - predicate1I is no longer declared as introduction rule, since it interferes with subsetI
Wed, 07 May 2008 10:56:37 +0200 - Explicitely applied predicate1I in a few proofs, because it is no longer
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
Wed, 07 May 2008 10:56:36 +0200 - Now imports Fun rather than Orderings
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.
Wed, 07 May 2008 10:56:35 +0200 Instantiated some rules to avoid problems with HO unification.
berghofe [Wed, 07 May 2008 10:56:35 +0200] rev 26793
Instantiated some rules to avoid problems with HO unification.
Wed, 07 May 2008 10:56:34 +0200 - Deleted code setup for finite and card
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
Wed, 07 May 2008 10:56:33 +0200 Instantiated subst 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.
Tue, 06 May 2008 23:33:05 +0200 converted "General logic setup";
wenzelm [Tue, 06 May 2008 23:33:05 +0200] rev 26790
converted "General logic setup";
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip