# HG changeset patch
# User paulson
# Date 844677110 -7200
# Node ID 4d7a4b25a11f73ff0ec8c5fcf312c93290c37291
# Parent  93c093620c28fec7dc2d7be30f46166f981f9827
Ran expandshort

diff -r 93c093620c28 -r 4d7a4b25a11f src/HOL/Lambda/Commutation.ML
--- a/src/HOL/Lambda/Commutation.ML	Mon Oct 07 10:28:44 1996 +0200
+++ b/src/HOL/Lambda/Commutation.ML	Mon Oct 07 10:31:50 1996 +0200
@@ -89,12 +89,12 @@
 goalw Commutation.thy [square_def,commute_def,diamond_def,Church_Rosser_def]
   "Church_Rosser(R) = confluent(R)";
 by (rtac iffI 1);
- by(fast_tac (HOL_cs addIs
+ by (fast_tac (HOL_cs addIs
       [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
        rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
 by (safe_tac HOL_cs);
 by (etac rtrancl_induct 1);
- by(Fast_tac 1);
+ by (Fast_tac 1);
 by (slow_best_tac (!claset addIs [r_into_rtrancl]
                     addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1);
 qed "Church_Rosser_confluent";
diff -r 93c093620c28 -r 4d7a4b25a11f src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Mon Oct 07 10:28:44 1996 +0200
+++ b/src/HOL/Lambda/Eta.ML	Mon Oct 07 10:31:50 1996 +0200
@@ -121,8 +121,14 @@
 
 goalw Eta.thy [square_def,id_def]  "square eta eta (eta^=) (eta^=)";
 by (rtac (impI RS allI RS allI) 1);
+by (Simp_tac 1);
 by (etac eta.induct 1);
-by (ALLGOALS(fast_tac (!claset addSEs [eta_decr,not_free_eta] addss !simpset)));
+by (best_tac (!claset addSIs [eta_decr]
+                      addIs [free_eta RS iffD1] addss !simpset) 1);
+by (slow_tac (!claset) 1);
+by (slow_tac (!claset) 1);
+by (slow_tac (!claset addSIs [eta_decr]
+                     addIs [free_eta RS iffD1]) 1);
 val lemma = result();
 
 goal Eta.thy "confluent(eta)";
@@ -226,50 +232,50 @@
 
 goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)";
 by (db.induct_tac "s" 1);
-  by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-  by(SELECT_GOAL(safe_tac HOL_cs)1);
-   by(res_inst_tac [("m","nat"),("n","i")] nat_less_cases 1);
-     by(res_inst_tac [("x","Var nat")] exI 1);
-     by(Asm_simp_tac 1);
-    by(fast_tac HOL_cs 1);
-   by(res_inst_tac [("x","Var(pred nat)")] exI 1);
-   by(Asm_simp_tac 1);
-  br notE 1;
-   ba 2;
-  be thin_rl 1;
-  by(res_inst_tac [("db","t")] db_case_distinction 1);
-    by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-    by(fast_tac (HOL_cs addDs [less_not_refl2]) 1);
-   by(Simp_tac 1);
-  by(Simp_tac 1);
- by(asm_simp_tac (!simpset addsimps [de_Morgan_disj]) 1);
- be thin_rl 1;
- be thin_rl 1;
- br allI 1;
- br iffI 1;
-  by(REPEAT(eresolve_tac [conjE,exE] 1));
-  by(rename_tac "u1 u2" 1);
-  by(res_inst_tac [("x","u1@u2")] exI 1);
-  by(Asm_simp_tac 1);
- be exE 1;
- be rev_mp 1;
- by(res_inst_tac [("db","t")] db_case_distinction 1);
-   by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-  by(Simp_tac 1);
-  by(fast_tac HOL_cs 1);
- by(Simp_tac 1);
+  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+  by (SELECT_GOAL(safe_tac HOL_cs)1);
+   by (res_inst_tac [("m","nat"),("n","i")] nat_less_cases 1);
+     by (res_inst_tac [("x","Var nat")] exI 1);
+     by (Asm_simp_tac 1);
+    by (fast_tac HOL_cs 1);
+   by (res_inst_tac [("x","Var(pred nat)")] exI 1);
+   by (Asm_simp_tac 1);
+  by (rtac notE 1);
+   by (assume_tac 2);
+  by (etac thin_rl 1);
+  by (res_inst_tac [("db","t")] db_case_distinction 1);
+    by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+    by (fast_tac (HOL_cs addDs [less_not_refl2]) 1);
+   by (Simp_tac 1);
+  by (Simp_tac 1);
+ by (asm_simp_tac (!simpset addsimps [de_Morgan_disj]) 1);
+ by (etac thin_rl 1);
+ by (etac thin_rl 1);
+ by (rtac allI 1);
+ by (rtac iffI 1);
+  by (REPEAT(eresolve_tac [conjE,exE] 1));
+  by (rename_tac "u1 u2" 1);
+  by (res_inst_tac [("x","u1@u2")] exI 1);
+  by (Asm_simp_tac 1);
+ by (etac exE 1);
+ by (etac rev_mp 1);
+ by (res_inst_tac [("db","t")] db_case_distinction 1);
+   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+  by (Simp_tac 1);
+  by (fast_tac HOL_cs 1);
+ by (Simp_tac 1);
 by (Asm_simp_tac 1);
 by (etac thin_rl 1);
 by (rtac allI 1);
 by (rtac iffI 1);
- be exE 1;
- by(res_inst_tac [("x","Fun t")] exI 1);
- by(Asm_simp_tac 1);
+ by (etac exE 1);
+ by (res_inst_tac [("x","Fun t")] exI 1);
+ by (Asm_simp_tac 1);
 by (etac exE 1);
 by (etac rev_mp 1);
 by (res_inst_tac [("db","t")] db_case_distinction 1);
-  by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
- by(Simp_tac 1);
+  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+ by (Simp_tac 1);
 by (Simp_tac 1);
 by (fast_tac HOL_cs 1);
 qed_spec_mp "not_free_iff_lifted";
diff -r 93c093620c28 -r 4d7a4b25a11f src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Mon Oct 07 10:28:44 1996 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Mon Oct 07 10:31:50 1996 +0200
@@ -58,12 +58,12 @@
 goal ParRed.thy
   "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
 by (db.induct_tac "t" 1);
-  by(asm_simp_tac (addsplit(!simpset)) 1);
- by(strip_tac 1);
- bes par_beta_cases 1;
-  by(Asm_simp_tac 1);
- by(asm_simp_tac (!simpset addsimps [subst_subst RS sym]) 1);
- by(fast_tac (!claset addSIs [par_beta_lift] addss (!simpset)) 1);
+  by (asm_simp_tac (addsplit(!simpset)) 1);
+ by (strip_tac 1);
+ by (eresolve_tac par_beta_cases 1);
+  by (Asm_simp_tac 1);
+ by (asm_simp_tac (!simpset addsimps [subst_subst RS sym]) 1);
+ by (fast_tac (!claset addSIs [par_beta_lift] addss (!simpset)) 1);
 by (fast_tac (!claset addss (!simpset)) 1);
 qed_spec_mp "par_beta_subst";
 
@@ -80,10 +80,10 @@
 
 goal ParRed.thy "!t. s => t --> t => cd s";
 by (db.induct_tac "s" 1);
-  by(Simp_tac 1);
- be rev_mp 1;
- by(db.induct_tac "db1" 1);
- by(ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] addss !simpset)));
+  by (Simp_tac 1);
+ by (etac rev_mp 1);
+ by (db.induct_tac "db1" 1);
+ by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] addss !simpset)));
 qed_spec_mp "par_beta_cd";
 
 (*** Confluence (via cd) ***)