2008-05-07 berghofe [Wed, 07 May 2008 10:56:52 +0200] rev 26803
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
to_set and to_pred attributes, because it is no longer applied automatically
- Manually applied predicate1I in proof of accp_subset, because it is no longer
part of the claset
- Replaced psubset_def by less_le
src/HOL/Wellfounded.thy

2008-05-07 berghofe [Wed, 07 May 2008 10:56:50 +0200] rev 26802
Deleted instantiation "set :: (type) itself".
src/HOL/Typedef.thy

2008-05-07 berghofe [Wed, 07 May 2008 10:56:49 +0200] rev 26801
- Function dec in Trancl_Tac must eta-contract relation before calling
decr, since it is now a function and could therefore be in eta-expanded form
- The trancl prover now does more eta-contraction itself, so eta-contraction
is no longer necessary in Tranclp_tac.
src/HOL/Transitive_Closure.thy

2008-05-07 berghofe [Wed, 07 May 2008 10:56:43 +0200] rev 26800
- Now uses Orderings as parent theory
- "'a set" is now just a type abbreviation for "'a => bool"
- The instantiation "set :: (type) ord" and the definition of (p)subset is
no longer needed, since it is subsumed by the order on functions and booleans.
The derived theorems (p)subset_eq can be used as a replacement.
- mem_Collect_eq and Collect_mem_eq can now be derived from the definitions
of mem and Collect.
- Replaced the instantiation "set :: (type) minus" by the two instantiations
"fun :: (type, minus) minus" and "bool :: minus". The theorem set_diff_eq
can be used as a replacement for the definition set_diff_def
- Replaced the instantiation "set :: (type) uminus" by the two instantiations
"fun :: (type, uminus) uminus" and "bool :: uminus". The theorem Compl_eq
can be used as a replacement for the definition Compl_def.
- Variable P in rule split_if must be instantiated manually in proof of
split_if_mem2 due to problems with HO unification
- Moved definition of dense linear orders and proofs about LEAST from
Orderings to Set
- Deleted code setup for sets
src/HOL/Set.thy

2008-05-07 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
src/HOL/Relation_Power.thy

2008-05-07 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.
src/HOL/Product_Type.thy

2008-05-07 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
src/HOL/Predicate.thy

2008-05-07 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
src/HOL/Orderings.thy

2008-05-07 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
src/HOL/List.thy

2008-05-07 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.
src/HOL/Lattices.thy