# HG changeset patch
# User oheimb
# Date 945975590 -3600
# Node ID 1c8de414b45db523f3de59992bca97276004a969
# Parent  908aca49c1a5d629712aa785e6beaa90fa535fff
removed inj_eq from the default simpset again

diff -r 908aca49c1a5 -r 1c8de414b45d src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Thu Dec 23 16:55:27 1999 +0100
+++ b/src/HOL/Finite.ML	Thu Dec 23 19:59:50 1999 +0100
@@ -134,7 +134,7 @@
 by (Clarify_tac 1);
 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
  by (Clarify_tac 1);
- by (full_simp_tac (simpset() addsimps [inj_on_def]delsimps[inj_eq]) 1);
+ by (full_simp_tac (simpset() addsimps [inj_on_def]) 1);
  by (Blast_tac 1);
 by (thin_tac "ALL A. ?PP(A)" 1);
 by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
@@ -822,7 +822,7 @@
 by (rtac funcsetI 1);
 (* arity *)
 by (auto_tac (claset() addSEs [equalityE], 
-	      simpset() addsimps [inj_on_def, restrict_def]delsimps[inj_eq]));
+	      simpset() addsimps [inj_on_def, restrict_def]));
 by (stac Diff_insert0 1);
 by Auto_tac;
 qed "constr_bij";
diff -r 908aca49c1a5 -r 1c8de414b45d src/HOL/Fun.ML
--- 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";