# HG changeset patch
# User paulson
# Date 962273967 -7200
# Node ID b86ff604729f45aa7b857fb409bbeb9a37bba6c9
# Parent  69b71b554e91a3f98739512a78a32ba4ade332fe
tidied proofs using default rule equalityCE

diff -r 69b71b554e91 -r b86ff604729f src/HOL/UNITY/Deadlock.ML
--- a/src/HOL/UNITY/Deadlock.ML	Thu Jun 29 12:17:18 2000 +0200
+++ b/src/HOL/UNITY/Deadlock.ML	Thu Jun 29 12:19:27 2000 +0200
@@ -18,10 +18,9 @@
 Goal "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)";
 by (induct_tac "n" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc])));
-by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1);
+by Auto_tac;
 qed "Collect_le_Int_equals";
 
-
 (*Dual of the required property.  Converse inclusion fails.*)
 Goal "(UN i: lessThan n. A i) Int (- A n) <=  \
 \     (UN i: lessThan n. (A i) Int (- A (Suc i)))";
diff -r 69b71b554e91 -r b86ff604729f src/HOL/UNITY/ELT.ML
--- a/src/HOL/UNITY/ELT.ML	Thu Jun 29 12:17:18 2000 +0200
+++ b/src/HOL/UNITY/ELT.ML	Thu Jun 29 12:19:27 2000 +0200
@@ -329,10 +329,8 @@
 by (blast_tac (claset() addIs [transient_strengthen]) 3);
 by (ALLGOALS (dres_inst_tac [("P1","P")] (impOfSubs preserves_subset_stable)));
 by (rewtac stable_def);
-by (blast_tac (claset() addSEs [equalityE]
-			addIs [constrains_Int RS constrains_weaken]) 2);
-by (blast_tac (claset() addSEs [equalityE]
-			addIs [constrains_Int RS constrains_weaken]) 1);
+by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 2);
+by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
 qed "gen_leadsETo_imp_Join_leadsETo";
 
 (*useful??*)
diff -r 69b71b554e91 -r b86ff604729f src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Thu Jun 29 12:17:18 2000 +0200
+++ b/src/HOL/UNITY/Extend.ML	Thu Jun 29 12:19:27 2000 +0200
@@ -45,7 +45,7 @@
 Goalw [Restrict_def]
      "[| A <= B;  Restrict B r = Restrict B s |] \
 \     ==> Restrict A r = Restrict A s";
-by (blast_tac (claset() addSEs [equalityE]) 1);
+by (Blast_tac 1);
 qed "Restrict_eq_mono";
 
 Goalw [Restrict_def, image_def]
diff -r 69b71b554e91 -r b86ff604729f src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Thu Jun 29 12:17:18 2000 +0200
+++ b/src/HOL/UNITY/Project.ML	Thu Jun 29 12:19:27 2000 +0200
@@ -435,7 +435,7 @@
 				       extend_set_Un_distrib]) 2);
 by (blast_tac (claset() addSIs [impOfSubs extend_set_project_set]) 2);
 by (full_simp_tac (simpset() addsimps [extend_set_def]) 1);
-by (blast_tac (claset() addSEs [equalityE]) 1);
+by (Blast_tac 1);
 (*The transient part*)
 by Auto_tac;
 by (force_tac (claset() addSDs [equalityD1]
diff -r 69b71b554e91 -r b86ff604729f src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Thu Jun 29 12:17:18 2000 +0200
+++ b/src/HOL/UNITY/Reach.ML	Thu Jun 29 12:19:27 2000 +0200
@@ -92,8 +92,8 @@
 
 Goalw [metric_def] "~ s x ==> Suc (metric (s(x:=True))) = metric s";
 by (subgoal_tac "{v. ~ (s(x:=True)) v} = {v. ~ s v} - {x}" 1);
-by Auto_tac;
-by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1);
+by (Force_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1);
 qed "Suc_metric";
 
 Goal "~ s x ==> metric (s(x:=True)) < metric s";
diff -r 69b71b554e91 -r b86ff604729f src/HOL/UNITY/Rename.ML
--- a/src/HOL/UNITY/Rename.ML	Thu Jun 29 12:17:18 2000 +0200
+++ b/src/HOL/UNITY/Rename.ML	Thu Jun 29 12:19:27 2000 +0200
@@ -145,7 +145,7 @@
 Goalw [surj_def] "surj (rename h) ==> surj h";
 by Auto_tac;
 by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1);
-by (auto_tac (claset() addSEs [equalityE], 
+by (auto_tac (claset(), 
 	      simpset() addsimps [program_equality_iff, raw_Acts_rename]));
 qed "surj_rename_imp_surj";
 
diff -r 69b71b554e91 -r b86ff604729f src/HOL/ex/PiSets.ML
--- a/src/HOL/ex/PiSets.ML	Thu Jun 29 12:17:18 2000 +0200
+++ b/src/HOL/ex/PiSets.ML	Thu Jun 29 12:19:27 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/PiSets.thy
+(*  Title:      HOL/ex/PiSets.ML
     ID:         $Id$
     Author:     Florian Kammueller, University of Cambridge
 
@@ -33,7 +33,7 @@
 by (assume_tac 1);
 by (rotate_tac 1 1);
 by (asm_full_simp_tac (simpset() addsimps [PiBij_def,restrict_apply1]) 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
+by (Blast_tac 1);
 qed "inj_PiBij";
 
 
diff -r 69b71b554e91 -r b86ff604729f src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Thu Jun 29 12:17:18 2000 +0200
+++ b/src/HOL/ex/set.ML	Thu Jun 29 12:19:27 2000 +0200
@@ -84,12 +84,12 @@
 (*** The Schroder-Berstein Theorem ***)
 
 Goal "[| -(f``X) = g``(-X);  f(a)=g(b);  a:X |] ==> b:X";
-by (blast_tac (claset() addEs [equalityE]) 1);
+by (Blast_tac 1);
 qed "disj_lemma";
 
 Goal "-(f``X) = g``(-X) ==> surj(%z. if z:X then f(z) else g(z))";
 by (asm_simp_tac (simpset() addsimps [surj_def]) 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
+by (Blast_tac 1);
 qed "surj_if_then_else";
 
 Goalw [inj_on_def]