# HG changeset patch
# User lcp
# Date 787846649 -3600
# Node ID c51c1f59e59ebd32e1e9e30cce715192a9232ddb
# Parent  3abd026e68a47047bf08b38fde36f2a0cd930f71
ran expandshort script

diff -r 3abd026e68a4 -r c51c1f59e59e src/ZF/IMP/Equiv.ML
--- a/src/ZF/IMP/Equiv.ML	Mon Dec 19 15:11:50 1994 +0100
+++ b/src/ZF/IMP/Equiv.ML	Mon Dec 19 15:17:29 1994 +0100
@@ -52,7 +52,7 @@
 goal Equiv.thy "!!c. <c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";
 
 (* start with rule induction *)
-be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
+by (etac (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1);
 
 by (rewrite_tac (Gamma_def::C_rewrite_rules));
 (* skip *)
@@ -89,7 +89,7 @@
 
 val [prem] = goal Equiv.thy
     "c : com ==> ALL x:C(c). <c,fst(x)> -c-> snd(x)";
-br (prem RS com.induct) 1;
+by (rtac (prem RS com.induct) 1);
 by (rewrite_tac C_rewrite_rules);
 by (safe_tac com_cs);
 by (ALLGOALS (asm_full_simp_tac ZF_ss));
@@ -107,7 +107,7 @@
 
 (* while *)
 by (EVERY1 [forward_tac [Gamma_bnd_mono], etac induct, atac]);
-by (rewrite_goals_tac [Gamma_def]);  
+by (rewtac Gamma_def);  
 by (safe_tac com_cs);
 by (EVERY1 [dtac bspec, atac]);
 by (ALLGOALS (asm_full_simp_tac ZF_ss));