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