expandshort

--- a/src/HOL/IMP/Transition.ML	Thu Dec 09 18:33:39 1999 +0100
+++ b/src/HOL/IMP/Transition.ML	Mon Dec 13 10:54:04 1999 +0100
@@ -209,21 +209,21 @@
 *)
 Goal "!c1 s. (c1;c2,s) -n-> (SKIP,t) --> \
 \     (? i1 i2 u. (c1,s) -i1-> (SKIP,u) & (c2,u) -i2-> (SKIP,t) & i1<n & i2<n)";
-by(induct_tac "n" 1);
+by (induct_tac "n" 1);
  by (fast_tac (claset() addSDs [hlemma]) 1);
-by(fast_tac (claset() addSIs [rel_pow_0_I,rel_pow_Suc_I2]
+by (fast_tac (claset() addSIs [rel_pow_0_I,rel_pow_Suc_I2]
                       addSDs [rel_pow_Suc_D2] addss simpset()) 1);
 qed_spec_mp "comp_decomp_lemma";
 
 Goal "!c s t. (c,s) -n-> (SKIP,t) --> <c,s> -c-> t";
-by(res_inst_tac [("n","n")] less_induct 1);
-by(Clarify_tac 1);
-be rel_pow_E2 1;
+by (res_inst_tac [("n","n")] less_induct 1);
+by (Clarify_tac 1);
+by (etac rel_pow_E2 1);
  by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
-by(exhaust_tac "c" 1);
+by (exhaust_tac "c" 1);
     by (fast_tac (claset() addSDs [hlemma]) 1);
-   by(Blast_tac 1);
-  by(blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);
- by(Blast_tac 1);
-by(Blast_tac 1);
+   by (Blast_tac 1);
+  by (blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "evalc1_impl_evalc";

--- a/src/HOL/List.ML	Thu Dec 09 18:33:39 1999 +0100
+++ b/src/HOL/List.ML	Mon Dec 13 10:54:04 1999 +0100
@@ -363,20 +363,20 @@
 qed_spec_mp "map_injective";
 
 Goal "inj f ==> inj (map f)";
-by(blast_tac (claset() addDs [map_injective,injD] addIs [injI]) 1);
+by (blast_tac (claset() addDs [map_injective,injD] addIs [injI]) 1);
 qed "inj_mapI";
 
 Goalw [inj_on_def] "inj (map f) ==> inj f";
-by(Clarify_tac 1);
-by(eres_inst_tac [("x","[x]")] ballE 1);
- by(eres_inst_tac [("x","[y]")] ballE 1);
-  by(Asm_full_simp_tac 1);
- by(Blast_tac 1);
-by(Blast_tac 1);
+by (Clarify_tac 1);
+by (eres_inst_tac [("x","[x]")] ballE 1);
+ by (eres_inst_tac [("x","[y]")] ballE 1);
+  by (Asm_full_simp_tac 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
 qed "inj_mapD";
 
 Goal "inj (map f) = inj f";
-by(blast_tac (claset() addDs [inj_mapD] addIs [inj_mapI]) 1);
+by (blast_tac (claset() addDs [inj_mapD] addIs [inj_mapI]) 1);
 qed "inj_map";
 
 (** rev **)
@@ -681,9 +681,9 @@
 qed_spec_mp "all_nth_imp_all_set";
 
 Goal "(!x : set xs. P x) = (!i. i<length xs --> P (xs ! i))";
-br iffI 1;
+by (rtac iffI 1);
  by (Asm_full_simp_tac 1);
-be all_nth_imp_all_set 1;
+by (etac all_nth_imp_all_set 1);
 qed_spec_mp "all_set_conv_all_nth";
 
 
@@ -967,28 +967,28 @@
  by (Simp_tac 1);
 by (Clarify_tac 1);
 by (exhaust_tac "xs" 1);
- by(Auto_tac);
+ by (Auto_tac);
 qed_spec_mp "length_zip";
 Addsimps [length_zip];
 
 Goal
 "!xs. length xs = length us --> length ys = length vs --> \
 \     zip (xs@ys) (us@vs) = zip xs us @ zip ys vs";
-by(induct_tac "us" 1);
- by(Asm_full_simp_tac 1);
-by(Asm_full_simp_tac 1);
-by(Clarify_tac 1);
-by(exhaust_tac "xs" 1);
- by(Auto_tac);
+by (induct_tac "us" 1);
+ by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (exhaust_tac "xs" 1);
+ by (Auto_tac);
 qed_spec_mp "zip_append";
 
 Goal "!xs. length xs = length ys --> zip (rev xs) (rev ys) = rev (zip xs ys)";
-by(induct_tac "ys" 1);
- by(Asm_full_simp_tac 1);
-by(Asm_full_simp_tac 1);
-by(Clarify_tac 1);
-by(exhaust_tac "xs" 1);
- by(Auto_tac);
+by (induct_tac "ys" 1);
+ by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (exhaust_tac "xs" 1);
+ by (Auto_tac);
 by (asm_full_simp_tac (simpset() addsimps [zip_append]) 1);
 qed_spec_mp "zip_rev";
 
@@ -997,23 +997,23 @@
 by (induct_tac "ys" 1);
  by (Simp_tac 1);
 by (Clarify_tac 1);
-by(exhaust_tac "xs" 1);
- by(Auto_tac);
+by (exhaust_tac "xs" 1);
+ by (Auto_tac);
 by (asm_full_simp_tac (simpset() addsimps (thms"nth.simps") addsplits [nat.split]) 1);
 qed_spec_mp "nth_zip";
 Addsimps [nth_zip];
 
 Goal
  "length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]";
-by(rtac sym 1);
-by(asm_simp_tac (simpset() addsimps [update_zip]) 1);
+by (rtac sym 1);
+by (asm_simp_tac (simpset() addsimps [update_zip]) 1);
 qed_spec_mp "zip_update";
 
 Goal "!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)";
 by (induct_tac "i" 1);
- by(Auto_tac);
+ by (Auto_tac);
 by (exhaust_tac "j" 1);
- by(Auto_tac);
+ by (Auto_tac);
 qed "zip_replicate";
 Addsimps [zip_replicate];
 
@@ -1245,11 +1245,11 @@
 Addsimps [set_replicate];
 
 Goal "set(replicate n x) = (if n=0 then {} else {x})";
-by(Auto_tac);
+by (Auto_tac);
 qed "set_replicate_conv_if";
 
 Goal "x : set(replicate n y) --> x=y";
-by(asm_simp_tac (simpset() addsimps [set_replicate_conv_if]) 1);
+by (asm_simp_tac (simpset() addsimps [set_replicate_conv_if]) 1);
 qed_spec_mp "in_set_replicateD";