isatool expandshort;

--- a/src/HOL/Induct/Acc.ML	Tue Jul 21 08:54:09 1998 +0200
+++ b/src/HOL/Induct/Acc.ML	Tue Jul 21 12:12:52 1998 +0200
@@ -25,12 +25,12 @@
 qed "acc_downward";
 
 Goal "(b,a) : r^* ==> a : acc r --> b : acc r";
-be rtrancl_induct 1;
-by(Blast_tac 1);
- by(blast_tac (claset() addDs [acc_downward]) 1);
+by (etac rtrancl_induct 1);
+by (Blast_tac 1);
+ by (blast_tac (claset() addDs [acc_downward]) 1);
 val lemma = result();
 Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r";
-by(blast_tac (claset() addDs [lemma]) 1);
+by (blast_tac (claset() addDs [lemma]) 1);
 qed "acc_downwards";
 
 val [major,indhyp] = goal Acc.thy

--- a/src/HOL/Lambda/ParRed.ML	Tue Jul 21 08:54:09 1998 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Tue Jul 21 12:12:52 1998 +0200
@@ -83,9 +83,9 @@
 Addsimps cd.rules;
 
 Goal "!t. s => t --> t => cd s";
-by(res_inst_tac[("u","s")] cd.induct 1);
-by(Auto_tac);
-by(fast_tac (claset() addSIs [par_beta_subst]) 1);
+by (res_inst_tac[("u","s")] cd.induct 1);
+by (Auto_tac);
+by (fast_tac (claset() addSIs [par_beta_subst]) 1);
 qed_spec_mp "par_beta_cd";
 
 (*** Confluence (via cd) ***)

--- a/src/HOL/Lex/MaxChop.ML	Tue Jul 21 08:54:09 1998 +0200
+++ b/src/HOL/Lex/MaxChop.ML	Tue Jul 21 12:12:52 1998 +0200
@@ -83,8 +83,8 @@
 by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
                         addsplits [split_split]) 1);
 by (Clarify_tac 1);
-by(rename_tac "xs1 ys1 xss1 ys" 1);
-by(split_asm_tac [split_list_case_asm] 1);
+by (rename_tac "xs1 ys1 xss1 ys" 1);
+by (split_asm_tac [split_list_case_asm] 1);
  by (Asm_full_simp_tac 1);
  by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
  by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
@@ -93,7 +93,7 @@
  by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
  by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
 by (Clarify_tac 1);
-by(rename_tac "us uss" 1);
+by (rename_tac "us uss" 1);
 by (subgoal_tac "xs1=us" 1);
  by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);

--- a/src/ZF/Update.ML	Tue Jul 21 08:54:09 1998 +0200
+++ b/src/ZF/Update.ML	Tue Jul 21 12:12:52 1998 +0200
@@ -20,7 +20,7 @@
 by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb]) 1);
 by (rtac fun_extension 1);
 by (best_tac (claset() addIs [apply_type, if_type, lam_type]) 1);
-ba 1;
+by (assume_tac 1);
 by (Asm_simp_tac 1);
 qed "update_idem";
 

--- a/src/ZF/ex/Integ.ML	Tue Jul 21 08:54:09 1998 +0200
+++ b/src/ZF/ex/Integ.ML	Tue Jul 21 12:12:52 1998 +0200
@@ -140,7 +140,7 @@
 
 Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))";
 by (asm_simp_tac (simpset() addsimps [zminus]) 1);
-by(blast_tac (claset() addIs [nat_0_le]) 1);
+by (blast_tac (claset() addIs [nat_0_le]) 1);
 qed "znegative_zminus_znat";