Lookup and union operations on terms are now modulo eta conversion.

Terms returned by decomp are now eta-contracted.

Added function for computing instantiation for the subst rule, which is used in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with HO unification.

eq_assumption now uses aeconv instead of aconv.

- Removed function eta_contract_atom, which did not quite work - Corrected and simplified function aeconv

Replaced Pattern.eta_contract_atom by Envir.eta_contract.

Removed instantiation for set.

Explicitely applied ext in proof of tnd.

Deleted subset_antisym in a few proofs, because it is accidentally applied to predicates as well.

- Tuned imports - Replaced blast by simp in proof of Stable_final_E_NOT_empty, since blast looped because of the new encoding of sets.

Manually applied subset_antisym in proof of Compl_fixedpoint, because it is accidentally applied to predicates as well.

Replaced blast by fast in proof of INT_Un_Compl_subset, since blast looped because of the new encoding of sets.

Functions get_branching_types and get_arities now use fold instead of foldl/r.

Temporarily disabled invocations of new code generator that do no longer work due to the encoding of sets as predicates

Replaced instance "set :: (plus) plus" by "fun :: (type, type) plus"

- Deleted arity proofs for set - Produce specific instances of theorems insert_eqvt, set_eqvt and perm_set_eq

Replaced union_empty2 by Un_empty_right.

Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that it gets applied to sets as well.

Deleted instance "set :: ({heap, finite}) heap"

- Declared subset_eq as code lemma - Deleted types_code declaration for sets

Deleted instantiation "set :: (enum) enum"

Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with definitions of + and * on functions.

Rephrased calculational proofs to avoid problems with HO unification

Rephrased forward proofs to avoid problems with HO unification

Rephrased proof of ann_hoare_case_analysis, to avoid problems with HO unification

Locally deleted some definitions that were applied too eagerly because of eta-expansion

- Instantiated parts_insert_substD to avoid problems with HO unification - Replaced auto by fastsimp in proof of parts_invKey, since auto looped because of the new encoding of sets

Instantiated parts_insert_substD to avoid problems with HO unification

Replaced blast by fast in proof of parts_singleton, since blast looped because of the new encoding of sets.

Adapted to encoding of sets as predicates

Replaced forward proofs of existential statements by backward proofs to avoid problems with HO unification

Adapted functions mk_setT and dest_setT to encoding of sets as predicates.

- 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

Deleted instantiation "set :: (type) itself".

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

- 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

Deleted instance "set :: (type) power" and moved instance "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.

- 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

- 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

- 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

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

Instantiated some rules to avoid problems with HO unification.

- 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

Instantiated subst rule to avoid problems with HO unification.

converted "General logic setup";

misc fixes and tuning;

updated generated file;

proper scoping of railaliases;

moved some railaliases here -- for proper scoping;

element: isakeyword markup;

removed isasymIN -- already defined in isar.sty;

added isasymIN/STRUCTURE;

converted generic.tex to Thy/Generic.thy;

removed isasymIMPORTS/BEGIN -- already defined in isar.sty;

tuned syntax: props and facts;