# HG changeset patch
# User nipkow
# Date 814371417 -3600
# Node ID 6eb89a693e05774ffba9802aaa344c2c81608568
# Parent  84f44b84d584a77b73837cb6a91b09e5507afb8f
Improved a few proofs.

diff -r 84f44b84d584 -r 6eb89a693e05 src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Thu Oct 19 13:25:03 1995 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Sun Oct 22 15:16:57 1995 +0100
@@ -105,7 +105,7 @@
 by (excluded_middle_tac "nat < i" 1);
 by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
 by (ALLGOALS(asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI])));
-qed"lift_lift";
+bind_thm("lift_lift", result() RS spec RS spec RS mp);
 
 goal Lambda.thy "!i j s. j < Suc i --> \
 \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
@@ -155,8 +155,7 @@
 goal Lambda.thy "!i j u v. i < Suc j --> \
 \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
 by(db.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps
-                   [lift_lift RS spec RS spec RS mp RS sym,lift_subst_lt])));
+by(ALLGOALS(asm_simp_tac(!simpset addsimps [lift_lift RS sym,lift_subst_lt])));
 by(strip_tac 1);
 by (excluded_middle_tac "nat < Suc(Suc j)" 1);
 by(Asm_full_simp_tac 1);
diff -r 84f44b84d584 -r 6eb89a693e05 src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Thu Oct 19 13:25:03 1995 +0100
+++ b/src/HOL/Lambda/ParRed.ML	Sun Oct 22 15:16:57 1995 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Lambda/ParRed.thy
+(*  Title:      HOL/Lambda/ParRed.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1995 TU Muenchen
@@ -63,8 +63,7 @@
  by(strip_tac 1);
  bes par_beta_cases 1;
   by(Asm_simp_tac 1);
- by(Asm_simp_tac 1);
- br (zero_less_Suc RS subst_subst RS subst) 1;
+ by(asm_simp_tac (!simpset addsimps [subst_subst RS sym]) 1);
  by(fast_tac (parred_cs addSIs [par_beta_lift] addss (!simpset)) 1);
 by(fast_tac (parred_cs addss (!simpset)) 1);
 bind_thm("par_beta_subst",
@@ -73,9 +72,7 @@
 (*** Confluence (directly) ***)
 
 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
-by(REPEAT(rtac allI 1));
-br impI 1;
-be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
+br par_beta.mutual_induct 1;
 by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst])));
 qed "diamond_par_beta";