Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Lex/AutoChopper.ML
changeset 2056 93c093620c28
parent 1950 97f1c6bf3ace
child 2609 4370e5f0fa3f 
--- a/src/HOL/Lex/AutoChopper.ML	Mon Oct 07 10:26:00 1996 +0200
+++ b/src/HOL/Lex/AutoChopper.ML	Mon Oct 07 10:28:44 1996 +0200
@@ -31,10 +31,10 @@
 by (strip_tac 1);
 by (rtac conjI 1);
 by (Fast_tac 1);
-by(simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1);
+by (simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1);
 by (strip_tac 1);
-by(REPEAT(eresolve_tac [conjE,exE] 1));
-by(hyp_subst_tac 1);
+by (REPEAT(eresolve_tac [conjE,exE] 1));
+by (hyp_subst_tac 1);
 by (Simp_tac 1);
 by (case_tac "zsa = []" 1);
 by (Asm_simp_tac 1);
@@ -55,14 +55,14 @@
 by (list.induct_tac "xs" 1);
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
-by(rename_tac "vss lrst" 1);  
+by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by (rename_tac "vss lrst" 1);  
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (res_inst_tac[("xs","vss")] list_eq_cases 1);
- by(hyp_subst_tac 1);
- by(Simp_tac 1);
+ by (hyp_subst_tac 1);
+ by (Simp_tac 1);
  by (fast_tac (!claset addSDs [no_acc]) 1);
-by(hyp_subst_tac 1);
+by (hyp_subst_tac 1);
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 val step2_a = (result() repeat_RS spec) RS mp;
 
@@ -78,12 +78,12 @@
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
  by (Fast_tac 1);
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 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);
+by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by (rename_tac "vss lrst" 1);  
+by (Asm_simp_tac 1);
 by (strip_tac 1);
 by (case_tac "acc_prefix A (next A st a) list" 1);
- by(Asm_simp_tac 1);
+ by (Asm_simp_tac 1);
 by (subgoal_tac "r @ [a] ~= []" 1);
  by (Fast_tac 1);
 by (Simp_tac 1);
@@ -103,9 +103,9 @@
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by (strip_tac 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);
+ by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+ by (rename_tac "vss lrst" 1);  
+ by (Asm_simp_tac 1);
  by (case_tac "acc_prefix A (next A st a) list" 1);
   by (strip_tac 1);
   by (res_inst_tac [("f","%k.a#k")] ex_special 1);
@@ -117,7 +117,7 @@
  by (res_inst_tac [("x","[a]")] exI 1);
  by (Asm_simp_tac 1);
  by (subgoal_tac "r @ [a] ~= []" 1);
-  br sym 1;
+  by (rtac sym 1);
   by (Fast_tac 1);
  by (Simp_tac 1);
 by (strip_tac 1);
@@ -140,9 +140,9 @@
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
  by (Fast_tac 1);
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 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);
+by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by (rename_tac "vss lrst" 1);  
+by (Asm_simp_tac 1);
 by (strip_tac 1);
 by (case_tac "acc_prefix A (next A st a) list" 1);
  by (Asm_simp_tac 1);
@@ -152,8 +152,8 @@
   by (Fast_tac 2);
  by (Simp_tac 2);
 by (subgoal_tac "flat(yss) @ zs = list" 1);
- by(hyp_subst_tac 1);
- by(atac 1);
+ by (hyp_subst_tac 1);
+ by (atac 1);
 by (case_tac "yss = []" 1);
  by (Asm_simp_tac 1);
  by (hyp_subst_tac 1);
@@ -163,7 +163,7 @@
 by (hyp_subst_tac 1);
 by (Simp_tac 1);
 by (rtac trans 1);
- be step2_a 1;
+ by (etac step2_a 1);
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 val step2_d = (result() repeat_RS spec) RS mp;
 
@@ -181,7 +181,7 @@
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by (strip_tac 1);
 by (case_tac "acc_prefix A (next A st a) list" 1);
- br conjI 1;
+ by (rtac conjI 1);
   by (strip_tac 1);
   by (res_inst_tac [("f","%k.a#k")] ex_special 1);
   by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
@@ -190,7 +190,7 @@
    by (asm_simp_tac HOL_ss 1);
   by (res_inst_tac [("x","x")] exI 1);
   by (Asm_simp_tac 1);
-  br list_cases 1;
+  by (rtac list_cases 1);
    by (Simp_tac 1);
   by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
  by (strip_tac 1);
@@ -201,7 +201,7 @@
   by (asm_simp_tac HOL_ss 1);
  by (res_inst_tac [("x","x")] exI 1);
  by (Asm_simp_tac 1);
- br list_cases 1;
+ by (rtac list_cases 1);
   by (Simp_tac 1);
  by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
 by (Asm_simp_tac 1);
@@ -223,22 +223,20 @@
                        Chopper.is_longest_prefix_chopper_def]
  "is_auto_chopper(auto_chopper)";
 by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
- br mp 1;
-  be step2_b 2;
+ by (rtac mp 1);
+  by (etac step2_b 2);
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (rtac conjI 1);
- br mp 1;
-  be step2_c 2;
+ by (rtac mp 1);
+  by (etac step2_c 2);
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
- by (Fast_tac 1);
 by (rtac conjI 1);
  by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
 by (rtac conjI 1);
- br mp 1;
-  be step2_d 2;
+ by (rtac mp 1);
+  by (etac step2_d 2);
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (rtac mp 1);
- be step2_e 2;
+ by (etac step2_e 2);
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (Fast_tac 1);
 qed"auto_chopper_is_auto_chopper";
isabelle