- 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

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

- 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.

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.

- 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

- "'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

Deleted instance "set :: (type) power" and moved instance

"fun :: (type, type) power" to the beginning of the theory

"fun :: (type, type) power" to the beginning of the theory

split_beta is now declared as monotonicity rule, to allow bounded

quantifiers in introduction rules of inductive predicates.

quantifiers in introduction rules of inductive predicates.

- 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

- 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

- 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

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

- 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

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

- 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.

- 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.