--- a/src/HOL/UNITY/Extend.ML Tue Mar 09 11:01:39 1999 +0100
+++ b/src/HOL/UNITY/Extend.ML Tue Mar 09 11:09:01 1999 +0100
@@ -8,21 +8,6 @@
function g (forgotten) maps the extended state to the "extending part"
*)
- Goal "inj f ==> (f a : f``A) = (a : A)";
- by (blast_tac (claset() addDs [injD]) 1);
- qed "inj_image_mem_iff";
-
-
- Goal "inj f ==> (f``A = f``B) = (A = B)";
- by (blast_tac (claset() addSEs [equalityE]
- addDs [injD]) 1);
- qed "inj_image_eq_iff";
-
-
-val rinst = read_instantiate_sg (sign_of thy);
-
- (*** General lemmas ***)
-
Open_locale "Extend";
val slice_def = thm "slice_def";