--- a/src/HOL/Fun.ML Thu Dec 23 16:55:27 1999 +0100
+++ b/src/HOL/Fun.ML Thu Dec 23 19:59:50 1999 +0100
@@ -110,7 +110,6 @@
by (etac injD 1);
by (assume_tac 1);
qed "inj_eq";
-Addsimps[inj_eq];
Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
by (etac injD 1);
@@ -411,7 +410,7 @@
Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
\ ==> inj_on (compose A g f) A";
by (auto_tac (claset(),
- simpset() addsimps [inj_on_def, compose_eq] delsimps[inj_eq]));
+ simpset() addsimps [inj_on_def, compose_eq]));
qed "inj_on_compose";
@@ -463,8 +462,7 @@
Goal "[| f: A funcset B; inj_on f A; f `` A = B; x: A |] \
\ ==> (lam y: B. (Inv A f) y) (f x) = x";
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]
- delsimps[inj_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
by (rtac selectI2 1);
by Auto_tac;
qed "Inv_f_f";