src/HOL/Lex/AutoChopper.ML

--- a/src/HOL/Lex/AutoChopper.ML	Tue Jan 30 15:19:20 1996 +0100
+++ b/src/HOL/Lex/AutoChopper.ML	Tue Jan 30 15:24:36 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/Lex/AutoChopper.ML
+(*  Title:      HOL/Lex/AutoChopper.ML
     ID:         $Id$
-    Author: 	Richard Mayr & Tobias Nipkow
+    Author:     Richard Mayr & Tobias Nipkow
     Copyright   1995 TUM
 
 Main result: auto_chopper satisfies the is_auto_chopper specification.
@@ -27,7 +27,7 @@
 by (simp_tac (!simpset addcongs [conj_cong]) 1);
 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 by (strip_tac 1);
-br conjI 1;
+by (rtac conjI 1);
 by (fast_tac HOL_cs 1);
 by(simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1);
 by (strip_tac 1);
@@ -100,7 +100,7 @@
  by (fast_tac HOL_cs 1);
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by (strip_tac 1);
-br conjI 1;
+by (rtac conjI 1);
  by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
  by(rename_tac "vss lrst" 1);  
  by(Asm_simp_tac 1);
@@ -155,11 +155,11 @@
  by (Asm_simp_tac 1);
  by (hyp_subst_tac 1);
  by (fast_tac (HOL_cs addSDs [no_acc]) 1);
-be ((neq_Nil_conv RS iffD1) RS exE) 1;
-be exE 1;
+by (etac ((neq_Nil_conv RS iffD1) RS exE) 1);
+by (etac exE 1);
 by (hyp_subst_tac 1);
 by (Simp_tac 1);
-br trans 1;
+by (rtac trans 1);
  be step2_a 1;
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 val step2_d = (result() repeat_RS spec) RS mp;
@@ -204,14 +204,14 @@
 by (Asm_simp_tac 1);
 by (strip_tac 1);
 by (res_inst_tac [("x","[a]")] exI 1);
-br conjI 1;
+by (rtac conjI 1);
  by (subgoal_tac "r @ [a] ~= []" 1);
   by (fast_tac HOL_cs 1);
  by (Simp_tac 1);
-br list_cases 1;
+by (rtac list_cases 1);
  by (Simp_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [acc_prefix_def] addcongs[conj_cong]) 1);
-be thin_rl 1; (* speed up *)
+by (etac thin_rl 1); (* speed up *)
 by (fast_tac HOL_cs 1);
 val step2_e = (result() repeat_RS spec) RS mp;
 Addsimps[split_paired_All];
@@ -223,18 +223,18 @@
  br mp 1;
   be step2_b 2;
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-br conjI 1;
+by (rtac conjI 1);
  br mp 1;
   be step2_c 2;
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  by (fast_tac HOL_cs 1);
-br conjI 1;
+by (rtac conjI 1);
  by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
-br conjI 1;
+by (rtac conjI 1);
  br mp 1;
   be step2_d 2;
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-br mp 1;
+by (rtac mp 1);
  be step2_e 2;
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (fast_tac HOL_cs 1);