# HG changeset patch
# User paulson
# Date 971087025 -7200
# Node ID 3daeda3d3cd030ec6593043ce8bff998728c8bad
# Parent  59d6633835fa62b3293d663b4975df1d44dbb7ee
expandshort

diff -r 59d6633835fa -r 3daeda3d3cd0 src/HOL/BCV/DFA_Framework.ML
--- a/src/HOL/BCV/DFA_Framework.ML	Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/DFA_Framework.ML	Mon Oct 09 12:23:45 2000 +0200
@@ -23,23 +23,23 @@
  "[| order r; top r T; \
 \    wti_is_stable_topless r T step wti succs n A; \
 \    is_dfa r dfa step succs n A |] ==> is_bcv r T wti n A dfa";
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (dtac is_dfaD 1);
 by (assume_tac 1);
-by(Clarify_tac 1);
-br iffI 1;
- br bexI 1;
-  br conjI 1;
-   ba 1;
+by (Clarify_tac 1);
+by (rtac iffI 1);
+ by (rtac bexI 1);
+  by (rtac conjI 1);
+   by (assume_tac 1);
   by (asm_full_simp_tac
         (simpset() addsimps[wti_is_stable_toplessD,stables_def]) 1);
- ba 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac
+ by (assume_tac 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac
     (simpset() addsimps [imp_conjR,all_conj_distrib,wti_is_stable_toplessD,
                          stables_def] addcongs [conj_cong]) 1);
-by(dres_inst_tac [("x","ts")] bspec 1);
- ba 1;
+by (dres_inst_tac [("x","ts")] bspec 1);
+ by (assume_tac 1);
 by (force_tac (claset()addDs [le_listD],simpset()) 1);
 qed "is_bcv_dfa";
 
diff -r 59d6633835fa -r 3daeda3d3cd0 src/HOL/BCV/Err.ML
--- a/src/HOL/BCV/Err.ML	Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Err.ML	Mon Oct 09 12:23:45 2000 +0200
@@ -32,12 +32,12 @@
 
 
 Goal "order(le r) = order r";
-br iffI 1;
- by(stac order_def 1);
- by(blast_tac (claset() addDs [order_antisym,OK_le_err_OK RS iffD2]
+by (rtac iffI 1);
+ by (stac order_def 1);
+ by (blast_tac (claset() addDs [order_antisym,OK_le_err_OK RS iffD2]
                         addIs [order_trans,OK_le_err_OK RS iffD1]) 1);
-by(stac order_def 1);
-by(blast_tac (claset() addIs [le_err_refl,le_err_trans,le_err_antisym]
+by (stac order_def 1);
+by (blast_tac (claset() addIs [le_err_refl,le_err_trans,le_err_antisym]
                        addDs [order_refl]) 1);
 qed "order_le_err";
 AddIffs [order_le_err];
@@ -92,8 +92,8 @@
 
 Goalw [sl_def,esl_def]
   "!!L. semilat L ==> err_semilat(esl L)";
-by(split_all_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [semilat_errI]) 1);
+by (split_all_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [semilat_errI]) 1);
 qed "err_semilat_eslI";
 
 Goalw [acc_def,lesub_def,le_def,lesssub_def]
@@ -126,21 +126,21 @@
 Goalw [lift_def]
  "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S";
 by (asm_simp_tac (simpset() addsplits [err.split]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "lift_in_errI";
 
 (** lift2 **)
 
 Goalw [lift2_def,plussub_def] "Err +_(lift2 f) x = Err";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "Err_lift2";
 
 Goalw [lift2_def,plussub_def] "x +_(lift2 f) Err = Err";
-by(simp_tac (simpset() addsplits [err.split]) 1);
+by (simp_tac (simpset() addsplits [err.split]) 1);
 qed "lift2_Err";
 
 Goalw [lift2_def,plussub_def] "OK x +_(lift2 f) OK y = x +_f y";
-by(simp_tac (simpset() addsplits [err.split]) 1);
+by (simp_tac (simpset() addsplits [err.split]) 1);
 qed "OK_lift2_OK";
 
 Addsimps [Err_lift2,lift2_Err,OK_lift2_OK];
@@ -164,16 +164,16 @@
 
 Goalw [Err.sup_def,lift2_def,plussub_def]
  "(Err.sup f ex ey = OK z) = (? x y. ex = OK x & ey = OK y & f x y = z)";
-br iffI 1;
- by(Clarify_tac 2);
+by (rtac iffI 1);
+ by (Clarify_tac 2);
  by (Asm_simp_tac 2);
-by(asm_full_simp_tac (simpset() addsplits [err.split_asm]) 1);
+by (asm_full_simp_tac (simpset() addsplits [err.split_asm]) 1);
 qed "Err_sup_eq_OK_conv";
 AddIffs [Err_sup_eq_OK_conv];
 
 Goalw [Err.sup_def,lift2_def,plussub_def]
  "(Err.sup f ex ey = Err) = (ex=Err | ey=Err)";
-by(simp_tac (simpset() addsplits [err.split]) 1);
+by (simp_tac (simpset() addsplits [err.split]) 1);
 qed "Err_sup_eq_Err";
 AddIffs [Err_sup_eq_Err];
 
@@ -181,56 +181,56 @@
 (*** semilat (err A) (le r) f ***)
 
 Goal "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err";
-by(blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1);
+by (blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1);
 qed "semilat_le_err_Err_plus";
 
 Goal "[| x: err A; semilat(err A, le r, f) |] ==> x +_f Err = Err";
-by(blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1);
+by (blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1);
 qed "semilat_le_err_plus_Err";
 
 Addsimps [semilat_le_err_Err_plus,semilat_le_err_plus_Err];
 
 Goal "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] \
 \     ==> x <=_r z";
-br (OK_le_err_OK RS iffD1) 1;
-by(etac subst 1);
-by(Asm_simp_tac 1);
+by (rtac (OK_le_err_OK RS iffD1) 1);
+by (etac subst 1);
+by (Asm_simp_tac 1);
 qed "semilat_le_err_OK1";
 
 Goal "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] \
 \     ==> y <=_r z";
-br (OK_le_err_OK RS iffD1) 1;
-by(etac subst 1);
-by(Asm_simp_tac 1);
+by (rtac (OK_le_err_OK RS iffD1) 1);
+by (etac subst 1);
+by (Asm_simp_tac 1);
 qed "semilat_le_err_OK2";
 
 Goalw [order_def] "[| x=y; order r |] ==> x <=_r y";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "eq_order_le";
 
 Goal
  "[| x:A; y:A; semilat(err A, le r, fe) |] ==> \
 \ ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))";
-br iffI 1;
+by (rtac iffI 1);
  by (Clarify_tac 1);
- bd (OK_le_err_OK RS iffD2) 1;
- bd (OK_le_err_OK RS iffD2) 1;
- bd semilat_lub 1;
-      ba 1;
-     ba 1;
-    by(Asm_simp_tac 1); 
-   by(Asm_simp_tac 1); 
-  by(Asm_simp_tac 1); 
- by(Asm_full_simp_tac 1);
-by(case_tac "(OK x) +_fe (OK y)" 1);
- ba 1;
-by(rename_tac "z" 1);
-by(subgoal_tac "OK z: err A" 1);
-bd eq_order_le 1;
-  by(Blast_tac 1);
- by(blast_tac (claset() addDs [rotate_prems 3 (plus_le_conv RS iffD1)]) 1);
-by(etac subst 1);
-by(blast_tac (claset() addIs [closedD]) 1);
+ by (dtac (OK_le_err_OK RS iffD2) 1);
+ by (dtac (OK_le_err_OK RS iffD2) 1);
+ by (dtac semilat_lub 1);
+      by (assume_tac 1);
+     by (assume_tac 1);
+    by (Asm_simp_tac 1); 
+   by (Asm_simp_tac 1); 
+  by (Asm_simp_tac 1); 
+ by (Asm_full_simp_tac 1);
+by (case_tac "(OK x) +_fe (OK y)" 1);
+ by (assume_tac 1);
+by (rename_tac "z" 1);
+by (subgoal_tac "OK z: err A" 1);
+by (dtac eq_order_le 1);
+  by (Blast_tac 1);
+ by (blast_tac (claset() addDs [rotate_prems 3 (plus_le_conv RS iffD1)]) 1);
+by (etac subst 1);
+by (blast_tac (claset() addIs [closedD]) 1);
 qed "OK_plus_OK_eq_Err_conv";
 Addsimps [OK_plus_OK_eq_Err_conv];
 
@@ -238,7 +238,7 @@
 
 (* FIXME? *)
 Goal "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "all_bex_swap_lemma";
 AddIffs [all_bex_swap_lemma];
 
@@ -246,10 +246,10 @@
  "[| !A:AS. closed (err A) (lift2 f); AS ~= {}; \
 \    !A:AS.!B:AS. A~=B --> (!a:A.!b:B. a +_f b = Err) |] \
 \ ==> closed (err(Union AS)) (lift2 f)";
-by(Asm_full_simp_tac 1);
-by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
-by(Fast_tac 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (Fast_tac 1);
 qed "closed_err_Union_lift2I";
 
 (* If AS = {} the thm collapses to
@@ -259,32 +259,32 @@
  "[| !A:AS. err_semilat(A, r, f); AS ~= {}; \
 \    !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |] \
 \ ==> err_semilat(Union AS, r, f)";
-by(asm_full_simp_tac (simpset() addsimps [closed_err_Union_lift2I]) 1);
-br conjI 1;
- by(Blast_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [err_def]) 1);
-br conjI 1;
- by(Clarify_tac 1);
- by(rename_tac "A a u B b" 1);
- by(case_tac "A = B" 1);
-  by(Asm_full_simp_tac 1);
- by(Asm_full_simp_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
- by(rename_tac "A a u B b" 1);
- by(case_tac "A = B" 1);
-  by(Asm_full_simp_tac 1);
- by(Asm_full_simp_tac 1);
-by(Clarify_tac 1);
-by(rename_tac "A ya yb B yd z C c a b" 1);
-by(case_tac "A = B" 1);
- by(case_tac "A = C" 1);
-  by(Asm_full_simp_tac 1);
- by(rotate_tac ~1 1);
- by(Asm_full_simp_tac 1);
-by(rotate_tac ~1 1);
-by(case_tac "B = C" 1);
- by(Asm_full_simp_tac 1);
-by(rotate_tac ~1 1);
-by(Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [closed_err_Union_lift2I]) 1);
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [err_def]) 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (rename_tac "A a u B b" 1);
+ by (case_tac "A = B" 1);
+  by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (rename_tac "A a u B b" 1);
+ by (case_tac "A = B" 1);
+  by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (rename_tac "A ya yb B yd z C c a b" 1);
+by (case_tac "A = B" 1);
+ by (case_tac "A = C" 1);
+  by (Asm_full_simp_tac 1);
+ by (rotate_tac ~1 1);
+ by (Asm_full_simp_tac 1);
+by (rotate_tac ~1 1);
+by (case_tac "B = C" 1);
+ by (Asm_full_simp_tac 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
 qed "err_semilat_UnionI";
diff -r 59d6633835fa -r 3daeda3d3cd0 src/HOL/BCV/JType.ML
--- a/src/HOL/BCV/JType.ML	Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/JType.ML	Mon Oct 09 12:23:45 2000 +0200
@@ -5,26 +5,26 @@
 *)
 
 Goalw [lesub_def,subtype_def] "T [=_S T";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "subtype_refl";
 AddIffs [subtype_refl];
 
 Goalw [lesub_def,subtype_def,is_Class_def]
  "(T [=_S Integer) = (T = Integer)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "subtype_Int_conv";
 
 Goalw [lesub_def,subtype_def] "(Integer [=_S T) = (T = Integer)";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "Int_subtype_conv";
 
 Goalw [lesub_def,subtype_def,is_Class_def]
  "(T [=_S Void) = (T = Void)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "subtype_Void_conv";
 
 Goalw [lesub_def,subtype_def] "(Void [=_S T) = (T = Void)";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "Void_subtype_conv";
 
 AddIffs [subtype_Int_conv,Int_subtype_conv,
@@ -32,72 +32,72 @@
 
 Goalw [lesub_def,subtype_def,is_Class_def]
  "T [=_S NullT = (T=NullT)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "subtype_NullT_conv";
 
 Goalw [lesub_def,subtype_def,is_Class_def]
  "NullT [=_S T = (T=NullT | (? C. T = Class C))";
-by(simp_tac (simpset() addsplits [ty.split]) 1);
+by (simp_tac (simpset() addsplits [ty.split]) 1);
 qed "NullT_subtype_conv";
 
 AddIffs [NullT_subtype_conv,subtype_NullT_conv];
 
 Goalw [lesub_def,subtype_def,is_Class_def]
  "T [=_S Class C = (T=NullT | (? D. T = Class D & (D,C) : S^*))";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 qed "subtype_Class_conv";
 
 Goalw [lesub_def,subtype_def,refl_def]
  "Class D [=_S T = (? C. T = Class C & (D,C):S^*)";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "Class_subtype_conv";
 
 AddIffs [Class_subtype_conv,subtype_Class_conv];
 
 Goalw [lesub_def,subtype_def,is_Class_def]
  "[| A [=_S B; B [=_S C |] ==> A [=_S C";
-by(asm_full_simp_tac (simpset() addsplits [ty.split,ty.split_asm]) 1);
-by(blast_tac (claset() addDs [transD] addIs [rtrancl_trans]) 1);
+by (asm_full_simp_tac (simpset() addsplits [ty.split,ty.split_asm]) 1);
+by (blast_tac (claset() addDs [transD] addIs [rtrancl_trans]) 1);
 qed "subtype_transD";
 
 Goalw [order_def,subtype_def,lesub_def,is_Class_def]
  "acyclic S ==> order (subtype S)";
-bd acyclic_impl_antisym_rtrancl 1;
-by(auto_tac (claset() addIs [rtrancl_trans],simpset() addsimps [antisymD]) );
+by (dtac acyclic_impl_antisym_rtrancl 1);
+by (auto_tac (claset() addIs [rtrancl_trans],simpset() addsimps [antisymD]) );
 qed "acyclic_impl_order_subtype";
 
 Goalw [acc_def,lesssub_def]
  "wf(S^-1) ==> acc(subtype S)";
-by(dres_inst_tac [("p","S^-1 - Id")] wf_subset 1);
- by(Blast_tac 1);
-bd wf_trancl 1;
+by (dres_inst_tac [("p","S^-1 - Id")] wf_subset 1);
+ by (Blast_tac 1);
+by (dtac wf_trancl 1);
 by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
 by (Clarify_tac 1);
-by(rename_tac "M T" 1);
-by(case_tac "EX C. Class C : M" 1);
- by(case_tac "T" 2);
-    by(Blast_tac 2);
-   by(Blast_tac 2);
-  by(res_inst_tac [("x","T")] bexI 2);
-   by(Blast_tac 2);
-  ba 2;
- by(Blast_tac 2);
-by(eres_inst_tac [("x","{C. Class C : M}")] allE 1);
-by(Auto_tac);
-by(rename_tac "D" 1);
-by(res_inst_tac [("x","Class D")] bexI 1);
- by(atac 2);
+by (rename_tac "M T" 1);
+by (case_tac "EX C. Class C : M" 1);
+ by (case_tac "T" 2);
+    by (Blast_tac 2);
+   by (Blast_tac 2);
+  by (res_inst_tac [("x","T")] bexI 2);
+   by (Blast_tac 2);
+  by (assume_tac 2);
+ by (Blast_tac 2);
+by (eres_inst_tac [("x","{C. Class C : M}")] allE 1);
+by (Auto_tac);
+by (rename_tac "D" 1);
+by (res_inst_tac [("x","Class D")] bexI 1);
+ by (atac 2);
 by (Clarify_tac 1);
-by(cut_inst_tac [("r","S")] (standard(rtrancl_r_diff_Id RS sym)) 1);
-by(Asm_full_simp_tac 1);
-be rtranclE 1;
- by(Blast_tac 1);
-bd (converseI RS rtrancl_converseI) 1;
-by(subgoal_tac "(S-Id)^-1 = (S^-1 - Id)" 1);
- by(Blast_tac 2);
-by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_trancl2]) 1);
+by (cut_inst_tac [("r","S")] (standard(rtrancl_r_diff_Id RS sym)) 1);
+by (Asm_full_simp_tac 1);
+by (etac rtranclE 1);
+ by (Blast_tac 1);
+by (dtac rtrancl_converseI 1);
+by (subgoal_tac "(S-Id)^-1 = (S^-1 - Id)" 1);
+ by (Blast_tac 2);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_trancl2]) 1);
 qed "wf_converse_subcls1_impl_acc_subtype";
 
 Addsimps [is_type_def];
@@ -105,8 +105,8 @@
 Goalw [closed_def,plussub_def,lift2_def,err_def,JType.sup_def]
  "[| univalent S; acyclic S |] ==> \
 \ closed (err(types S)) (lift2 (JType.sup S))";
-by(simp_tac (simpset() addsplits [err.split,ty.split]) 1);
-by(blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD]
+by (simp_tac (simpset() addsplits [err.split,ty.split]) 1);
+by (blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD]
                        addSIs [is_ubI]) 1);
 qed "closed_err_types";
 
@@ -114,52 +114,52 @@
 
 Goalw [semilat_def,split RS eq_reflection,JType.esl_def,Err.sl_def]
  "[| univalent S; acyclic S |] ==> err_semilat (JType.esl S)";
-by(asm_full_simp_tac (simpset() addsimps [acyclic_impl_order_subtype,closed_err_types]) 1);
+by (asm_full_simp_tac (simpset() addsimps [acyclic_impl_order_subtype,closed_err_types]) 1);
 
-br conjI 1;
- by(Clarify_tac 1);
- by(case_tac "x" 1);
-  by(Clarify_tac 1);
-  by(Simp_tac 1);
- by(case_tac "y" 1);
-  by(Clarify_tac 1);
-  by(Simp_tac 1);
- by(fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (case_tac "x" 1);
+  by (Clarify_tac 1);
+  by (Simp_tac 1);
+ by (case_tac "y" 1);
+  by (Clarify_tac 1);
+  by (Simp_tac 1);
+ by (fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss
              (simpset() addsimps [plussub_def,lift2_def,JType.sup_def]
                         addsplits [ty.split])) 1);
 
-br conjI 1;
- by(Clarify_tac 1);
- by(case_tac "x" 1);
-  by(Clarify_tac 1);
-  by(Simp_tac 1);
- by(case_tac "y" 1);
-  by(Clarify_tac 1);
-  by(Simp_tac 1);
- by(fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (case_tac "x" 1);
+  by (Clarify_tac 1);
+  by (Simp_tac 1);
+ by (case_tac "y" 1);
+  by (Clarify_tac 1);
+  by (Simp_tac 1);
+ by (fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss
              (simpset() addsimps [plussub_def,lift2_def,JType.sup_def]
                         addsplits [ty.split])) 1);
 
-by(Clarify_tac 1);
-by(case_tac "x" 1);
- by(Clarify_tac 1);
-by(case_tac "y" 1);
- by(Clarify_tac 1);
-by(asm_simp_tac(simpset() addsimps [plussub_def,lift2_def,JType.sup_def]
+by (Clarify_tac 1);
+by (case_tac "x" 1);
+ by (Clarify_tac 1);
+by (case_tac "y" 1);
+ by (Clarify_tac 1);
+by (asm_simp_tac(simpset() addsimps [plussub_def,lift2_def,JType.sup_def]
                           addsplits [ty.split]) 1);
-br conjI 1;
- by(Blast_tac 1);
-br conjI 1;
- by(Blast_tac 1);
-br conjI 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD]
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD]
                        addSIs [is_ubI]) 1);
 qed "err_semilat_JType_esl";
 
diff -r 59d6633835fa -r 3daeda3d3cd0 src/HOL/BCV/JVM.ML
--- a/src/HOL/BCV/JVM.ML	Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/JVM.ML	Mon Oct 09 12:23:45 2000 +0200
@@ -13,7 +13,7 @@
        Listn.sl_def,upto_esl_def,JType.esl_def,Err.esl_def]
  "states S maxs maxr == opt(err((Union {list n (types S) |n. n <= maxs}) <*>\
 \                                list maxr (err(types S))))";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "JVM_states_unfold";
 
 Goalw [JVM.le_def,JVM.sl_def,Opt.sl_def,Err.sl_def,
@@ -21,70 +21,70 @@
        Listn.sl_def,upto_esl_def,JType.esl_def,Err.esl_def]
  "JVM.le S m n == \
 \ Opt.le(Err.le(Product.le(Listn.le(subtype S))(Listn.le(Err.le(subtype S)))))";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "JVM_le_unfold";
 
 Goalw [wfis_def,wfi_def]
  "[| wfis S md maxr bs; bs!p = Load n; p < size bs |] ==> n < maxr";
-by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
+by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
 qed "wf_LoadD";
 
 Goalw [wfis_def,wfi_def]
  "[| wfis S md maxr bs; bs!p = Store n; p < size bs |] ==> n < maxr";
-by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
+by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
 qed "wf_StoreD";
 
 Goalw [wfis_def,wfi_def]
  "[| wfis S md m bs; bs!p = New C; p < size bs |] ==> (C,Object):S^*";
-by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
+by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
 qed "wf_NewD";
 
 Goalw [wfis_def,wfi_def,wf_mdict_def]
  "[| wfis S md maxr bs; wf_mdict S md; bs!p = Invoke C m pT (Class R); \
 \    p < size bs |] ==> (R,Object):S^*";
-by(force_tac (claset(),simpset()addsimps [all_set_conv_all_nth]) 1);
+by (force_tac (claset(),simpset()addsimps [all_set_conv_all_nth]) 1);
 qed "wf_InvokeD";
 
 Goalw [wfis_def,wfi_def]
  "[|wfis S md m bs; bs!p = Getfield (Class C) D; p < size bs|] ==> \
 \ (C,Object):S^*";
-by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
+by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth]));
 qed "wf_GetfieldD";
 
 Goal "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "special_ex_swap_lemma";
 AddIffs [special_ex_swap_lemma];
 
 Goalw [pres_type_def,list_def,step_def,JVM_states_unfold]
  "[| wfis S md maxr bs; wf_mdict S md |] ==> \
 \ pres_type (step S maxs rT bs) (size bs) (states S maxs maxr)";
-by(clarify_tac (claset() addSEs [option_map_in_optionI,lift_in_errI]) 1);
-by(asm_simp_tac (simpset()addsimps [exec_def] addsplits [instr.split]) 1);
+by (clarify_tac (claset() addSEs [option_map_in_optionI,lift_in_errI]) 1);
+by (asm_simp_tac (simpset()addsimps [exec_def] addsplits [instr.split]) 1);
 
-br conjI 1;
-by(fast_tac (claset() addDs [refl RS nth_in] addSEs [wf_LoadD] addss
+by (rtac conjI 1);
+by (fast_tac (claset() addDs [refl RS nth_in] addSEs [wf_LoadD] addss
       (simpset() delsimps [is_type_def]addsplits [err.split])) 1);
 
-br conjI 1;
+by (rtac conjI 1);
 by (fast_tac (claset() addDs [set_update_subset_insert RS subsetD]
                addSEs [wf_StoreD] addss (simpset() addsplits [list.split])) 1);
 
-br conjI 1;
+by (rtac conjI 1);
 by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1);
 
-br conjI 1;
+by (rtac conjI 1);
 by (fast_tac (claset() addIs [wf_GetfieldD]
               addss (simpset() addsplits [list.split,ty.split])) 1);
 
-br conjI 1;
+by (rtac conjI 1);
 by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1);
 
-br conjI 1;
+by (rtac conjI 1);
 by (fast_tac (claset() addIs [wf_NewD] addss simpset()) 1);
 
-br conjI 1;
-by(DEPTH_SOLVE_1(rtac conjI 1 ORELSE
+by (rtac conjI 1);
+by (DEPTH_SOLVE_1(rtac conjI 1 ORELSE
     Clarify_tac 1 THEN asm_full_simp_tac (simpset() addsimps [wf_InvokeD]
       addsplits [list.split,ty.split,option.split]) 1));
 
@@ -100,60 +100,60 @@
 \    (step S maxs rT bs) \
 \    (wti S maxs rT bs) \
 \    (succs bs) (size bs) (states S maxs maxr)";
-by(simp_tac (simpset() addsplits [option.split]) 1);
-by(simp_tac (simpset() addsplits [err.split]) 1);
-by(Clarify_tac 1);
-br conjI 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-by(EVERY1[etac allE, mp_tac]);
-by(rewrite_goals_tac [exec_def,succs_def]);
-by(split_tac [instr.split] 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
+by (simp_tac (simpset() addsplits [err.split]) 1);
+by (Clarify_tac 1);
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (EVERY1[etac allE, mp_tac]);
+by (rewrite_goals_tac [exec_def,succs_def]);
+by (split_tac [instr.split] 1);
 
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split,err.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split,err.split]) 1);
 
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
 
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
 
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
 
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
-by(Blast_tac 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (Blast_tac 1);
 
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
 
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
 
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
 
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split,ty.split]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split,ty.split]) 1);
 
-br conjI 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
-by(Blast_tac 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1);
+by (Blast_tac 1);
 
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]
                                 addsimps [le_list_refl,le_err_refl] ) 1);
 qed "wti_is_stable_topless";
 
@@ -162,80 +162,80 @@
  "[| wfis S md maxr bs; wf_mdict S md |] ==> \
 \ mono (JVM.le S maxs maxr) (step S maxs rT bs) (size bs) (states S maxs maxr)";
 by (Clarify_tac 1);
-by(simp_tac (simpset() addsplits [option.split]) 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
 by (Clarify_tac 1);
-by(Asm_simp_tac 1);
-by(split_tac [err.split] 1);
-br conjI 1;
+by (Asm_simp_tac 1);
+by (split_tac [err.split] 1);
+by (rtac conjI 1);
  by (Clarify_tac 1);
 by (Clarify_tac 1);
-by(simp_tac (simpset() addsimps [exec_def] delsplits [split_if]) 1);
-by(split_tac [instr.split] 1);
+by (simp_tac (simpset() addsimps [exec_def] delsplits [split_if]) 1);
+by (split_tac [instr.split] 1);
 
-br conjI 1;
+by (rtac conjI 1);
 by (fast_tac (claset() addDs [le_listD] addSEs [wf_LoadD]
        addss (simpset() addsplits [err.split])) 1);
 
-br conjI 1;
+by (rtac conjI 1);
 by (fast_tac (claset() addIs [list_update_le_cong,le_listD] addSEs [wf_StoreD]
        addss (simpset() addsplits [list.split])) 1);
 
-br conjI 1;
-by(Asm_simp_tac 1);
+by (rtac conjI 1);
+by (Asm_simp_tac 1);
 
-br conjI 1;
-by(Asm_simp_tac 1);
+by (rtac conjI 1);
+by (Asm_simp_tac 1);
 
-br conjI 1;
-by(fast_tac (claset() addss (simpset() addsplits [list.split])) 1);
+by (rtac conjI 1);
+by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1);
 
-br conjI 1;
+by (rtac conjI 1);
 by (fast_tac (claset() addDs [rtrancl_trans]
        addss (simpset() addsplits [list.split])) 1);
 
-br conjI 1;
+by (rtac conjI 1);
  by (Clarify_tac 1);
- by(asm_full_simp_tac (simpset() addsplits [list.split]) 1);
- br conjI 1;
+ by (asm_full_simp_tac (simpset() addsplits [list.split]) 1);
+ by (rtac conjI 1);
   by (Clarify_tac 1);
  by (Clarify_tac 1);
- br conjI 1;
+ by (rtac conjI 1);
   by (Clarify_tac 1);
  by (Clarify_tac 1);
- br conjI 1;
+ by (rtac conjI 1);
   by (Clarify_tac 1);
  by (Clarify_tac 1);
- by(Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
  by (blast_tac (claset() addIs [rtrancl_trans,subtype_transD]) 1);
 
-br conjI 1;
-by(asm_full_simp_tac (simpset() addsimps [reflD] addsplits [list.split]) 1);
+by (rtac conjI 1);
+by (asm_full_simp_tac (simpset() addsimps [reflD] addsplits [list.split]) 1);
 
-br conjI 1;
+by (rtac conjI 1);
 (* 39 *)
  by (Clarify_tac 1);
- by(asm_full_simp_tac (simpset() addsplits [list.split]) 1);
+ by (asm_full_simp_tac (simpset() addsplits [list.split]) 1);
  by (blast_tac (claset() addIs [rtrancl_trans,subtype_transD]) 1);
 
-br conjI 1;
-by(fast_tac (claset() addss (simpset() addsplits [list.split,ty.split_asm]
+by (rtac conjI 1);
+by (fast_tac (claset() addss (simpset() addsplits [list.split,ty.split_asm]
                                        addsimps [is_Class_def,is_ref_def])) 1);
 
-by(asm_simp_tac (simpset() addsplits [list.split]) 1);
-by(blast_tac (claset() addIs [subtype_transD]) 1);
+by (asm_simp_tac (simpset() addsplits [list.split]) 1);
+by (blast_tac (claset() addIs [subtype_transD]) 1);
 
 qed "exec_mono";
 
 
 Goalw [JVM.sl_def,stk_esl_def,reg_sl_def]
  "[| univalent S; acyclic S |] ==> semilat(JVM.sl S maxs maxr)";
-by(REPEAT(ares_tac [semilat_opt,err_semilat_Product_esl,err_semilat_upto_esl,
+by (REPEAT(ares_tac [semilat_opt,err_semilat_Product_esl,err_semilat_upto_esl,
           err_semilat_eslI,semilat_Listn_sl,err_semilat_JType_esl] 1));
 qed "semilat_JVM_slI";
 
 Goal "JVM.sl S maxs maxr == \
 \     (states S maxs maxr, JVM.le S maxs maxr, JVM.sup S maxs maxr)";
-by(simp_tac (simpset() addsimps [states_def,JVM.le_def,JVM.sup_def,
+by (simp_tac (simpset() addsimps [states_def,JVM.le_def,JVM.sup_def,
       surjective_pairing RS sym]) 1);
 qed "sl_triple_conv";
 
@@ -244,18 +244,18 @@
 \    bounded (succs bs) (size bs) |] ==> \
 \ is_bcv (JVM.le S maxs maxr) (Some Err) (wti S maxs rT bs) \
 \        (size bs) (states S maxs maxr) (kiljvm S maxs maxr rT bs)";
-br is_bcv_kildall 1;
-      by(simp_tac (simpset() addsimps [symmetric sl_triple_conv]) 1);
-      by(blast_tac (claset() addSIs [semilat_JVM_slI] addDs [wf_acyclic]) 1);
-     by(simp_tac (simpset() addsimps [JVM_le_unfold]) 1);
-     by(blast_tac (claset()
+by (rtac is_bcv_kildall 1);
+      by (simp_tac (simpset() addsimps [symmetric sl_triple_conv]) 1);
+      by (blast_tac (claset() addSIs [semilat_JVM_slI] addDs [wf_acyclic]) 1);
+     by (simp_tac (simpset() addsimps [JVM_le_unfold]) 1);
+     by (blast_tac (claset()
        addSIs [acyclic_impl_order_subtype,wf_converse_subcls1_impl_acc_subtype]
        addDs [wf_acyclic]) 1);
-    by(simp_tac (simpset() addsimps [JVM_le_unfold]) 1);
-   be exec_pres_type 1;
-   ba 1;
-  ba 1;
- be exec_mono 1;
- ba 1;
-be wti_is_stable_topless 1;
+    by (simp_tac (simpset() addsimps [JVM_le_unfold]) 1);
+   by (etac exec_pres_type 1);
+   by (assume_tac 1);
+  by (assume_tac 1);
+ by (etac exec_mono 1);
+ by (assume_tac 1);
+by (etac wti_is_stable_topless 1);
 qed "is_bcv_kiljvm";
diff -r 59d6633835fa -r 3daeda3d3cd0 src/HOL/BCV/Kildall.ML
--- a/src/HOL/BCV/Kildall.ML	Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Kildall.ML	Mon Oct 09 12:23:45 2000 +0200
@@ -34,8 +34,8 @@
  "[| semilat(A,r,f) |] ==> \
 \ !xs. xs : list n A --> x : A --> (!p : set ps. p<n) \
 \      --> merges f x ps xs : list n A";
-by(ftac semilatDclosedI 1);
-by(rewtac closed_def);
+by (ftac semilatDclosedI 1);
+by (rewtac closed_def);
 by (induct_tac "ps" 1);
 by (Auto_tac);
 qed_spec_mp "merges_preserves_type";
@@ -49,9 +49,9 @@
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
 by (rtac order_trans 1);
-  by(Asm_simp_tac 1);
+  by (Asm_simp_tac 1);
  by (etac list_update_incr 1);
-   ba 1;
+   by (assume_tac 1);
   by (Asm_simp_tac 1);
  by (Asm_simp_tac 1);
 by (blast_tac (claset() addSIs [listE_set]
@@ -70,13 +70,13 @@
  by (rtac context_conjI 1);
   by (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs" 1);
    by (EVERY[etac subst 2, rtac merges_incr 2]);
-      by(force_tac (claset() addSDs [le_listD],
+      by (force_tac (claset() addSDs [le_listD],
                     simpset() addsimps [nth_list_update]) 1);
      by (assume_tac 1);
     by (blast_tac (claset() addSIs [listE_set]
                    addIs [closedD,listE_length RS nth_in]) 1);
-   ba 1;
-  by(Asm_simp_tac 1);
+   by (assume_tac 1);
+  by (Asm_simp_tac 1);
  by (Clarify_tac 1);
  by (rotate_tac ~2 1);
  by (asm_full_simp_tac (simpset() addsimps
@@ -108,7 +108,7 @@
 by (Clarify_tac 1);
 by (rotate_tac ~2 1);
 by (Asm_full_simp_tac 1);
-by(EVERY[etac allE 1, etac impE 1, etac mp 2]);
+by (EVERY[etac allE 1, etac impE 1, etac mp 2]);
  by (asm_simp_tac (simpset() addsimps [closedD]) 1);
 by (asm_full_simp_tac (simpset() addsimps [list_update_le_listI]) 1);
 val lemma = result();
@@ -125,9 +125,9 @@
 Goal "[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A --> \
 \     (!p:set ps. p<n) --> \
 \     (merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)";
-by(induct_tac "ps" 1);
+by (induct_tac "ps" 1);
  by (Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [nth_list_update,closedD,listE_nth_in]) 1);
+by (asm_simp_tac (simpset() addsimps [nth_list_update,closedD,listE_nth_in]) 1);
 qed_spec_mp "nth_merges";
 
 
@@ -137,14 +137,14 @@
 \ propa f qs t ss w = \
 \ (merges f t qs ss, {q. q:set qs & t +_f ss!q ~= ss!q} Un w)";
 by (induct_tac "qs" 1);
- by(Simp_tac 1);
+ by (Simp_tac 1);
 by (Simp_tac 1);
-by(Clarify_tac 1);
-br conjI 1;
+by (Clarify_tac 1);
+by (rtac conjI 1);
  by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
- by(Blast_tac 1);
+ by (Blast_tac 1);
 by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "decomp_propa";
 
 (** iter **)
@@ -152,17 +152,17 @@
 val [iter_wf,iter_tc] = iter.tcs;
 
 goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf));
-by(REPEAT(rtac wf_same_fstI 1));
-by(split_all_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1);
-by(REPEAT(rtac wf_same_fstI 1));
-br wf_lex_prod 1;
- br wf_finite_psubset 2; (* FIXME *)
-by(Clarify_tac 1);
-bd (semilatDorderI RS acc_le_listI) 1;
- ba 1;
-by(rewrite_goals_tac [acc_def,lesssub_def]);
-ba 1;
+by (REPEAT(rtac wf_same_fstI 1));
+by (split_all_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1);
+by (REPEAT(rtac wf_same_fstI 1));
+by (rtac wf_lex_prod 1);
+ by (rtac wf_finite_psubset 2); (* FIXME *)
+by (Clarify_tac 1);
+by (dtac (semilatDorderI RS acc_le_listI) 1);
+ by (assume_tac 1);
+by (rewrite_goals_tac [acc_def,lesssub_def]);
+by (assume_tac 1);
 qed "iter_wf";
 
 Goalw [lesssub_def]
@@ -170,28 +170,28 @@
 \ ss <[r] merges f t qs ss | \
 \ merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w";
 by (asm_simp_tac (simpset() addsimps [merges_incr]) 1);
-br impI 1;
-bd (sym RS (rotate_prems 4 (merges_same_conv RS iffD1))) 1;
-    ba 1;
-   ba 1;
-  ba 1;
- by(Asm_simp_tac 1);
+by (rtac impI 1);
+by (dtac (sym RS (rotate_prems 4 (merges_same_conv RS iffD1))) 1);
+    by (assume_tac 1);
+   by (assume_tac 1);
+  by (assume_tac 1);
+ by (Asm_simp_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]
                             addsimps [le_iff_plus_unchanged RS sym]) 1);
 by (blast_tac (claset() addSIs [psubsetI] addEs [equalityE]) 1);
 qed "inter_tc_lemma";
 
 goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_tc));
-by(asm_simp_tac (simpset() addsimps [same_fst_def,pres_type_def]) 1);
-by(clarify_tac (claset() delrules [disjCI]) 1);
-by(subgoal_tac "(@p. p:w) : w" 1);
+by (asm_simp_tac (simpset() addsimps [same_fst_def,pres_type_def]) 1);
+by (clarify_tac (claset() delrules [disjCI]) 1);
+by (subgoal_tac "(@p. p:w) : w" 1);
  by (fast_tac (claset() addIs [someI]) 2);
-by(subgoal_tac "ss : list (size ss) A" 1);
+by (subgoal_tac "ss : list (size ss) A" 1);
  by (blast_tac (claset() addSIs [listI]) 2);
-by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
+by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
  by (blast_tac (claset() addDs [boundedD]) 2);
-by(rotate_tac 1 1);
-by(asm_full_simp_tac (simpset() delsimps [listE_length]
+by (rotate_tac 1 1);
+by (asm_full_simp_tac (simpset() delsimps [listE_length]
       addsimps [decomp_propa,finite_psubset_def,inter_tc_lemma,
                 bounded_nat_set_is_finite]) 1);
 qed "iter_tc";
@@ -204,15 +204,15 @@
 \     --> P A r f step succs (merges f (step p (ss!p)) (succs p) ss) \
 \           ({q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))\
 \    ==> P A r f step succs ss w) ==> P A r f step succs ss w";
-by(res_inst_tac [("P","P")] (iter_tc RS (iter_wf RS iter.induct)) 1);
-by(rename_tac "w" 1);
-brs prems 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset()) 1);
-by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
- by(rotate_tac ~1 1);
- by(asm_full_simp_tac (simpset() addsimps [decomp_propa]) 1);
-by(subgoal_tac "(@p. p:w) : w" 1);
+by (res_inst_tac [("P","P")] (iter_tc RS (iter_wf RS iter.induct)) 1);
+by (rename_tac "w" 1);
+by (resolve_tac prems 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset()) 1);
+by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
+ by (rotate_tac ~1 1);
+ by (asm_full_simp_tac (simpset() addsimps [decomp_propa]) 1);
+by (subgoal_tac "(@p. p:w) : w" 1);
  by (fast_tac (claset() addIs [someI]) 2);
 by (blast_tac (claset() addDs [boundedD]) 1);
 qed "iter_induct";
@@ -227,9 +227,9 @@
 \        {q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))";
 by (rtac ((iter_tc RS (iter_wf RS (hd iter.simps))) RS trans) 1);
 by (Asm_simp_tac 1);
-br impI 1;
-by(stac decomp_propa 1);
- by(subgoal_tac "(@p. p:w) : w" 1);
+by (rtac impI 1);
+by (stac decomp_propa 1);
+ by (subgoal_tac "(@p. p:w) : w" 1);
   by (fast_tac (claset() addIs [someI]) 2);
  by (blast_tac (claset() addDs [boundedD]) 1);
 by (Simp_tac 1);
@@ -242,26 +242,26 @@
 \    q : set (succs p) --> step p (ss ! p) +_f ss ! q = ss ! q; \
 \    q ~: w | q = p  |] ==> \
 \      stable r step succs (merges f (step p (ss!p)) (succs p) ss) q";
-by(subgoal_tac "step p (ss!p) : A" 1);
+by (subgoal_tac "step p (ss!p) : A" 1);
  by (blast_tac (claset() addIs [listE_nth_in,pres_typeD]) 2);
 by (Simp_tac 1);
-by(Clarify_tac 1);
-by(stac nth_merges 1);
-     ba 1;
-    ba 1;
-   ba 2;
+by (Clarify_tac 1);
+by (stac nth_merges 1);
+     by (assume_tac 1);
+    by (assume_tac 1);
+   by (assume_tac 2);
   by (blast_tac (claset() addDs [boundedD]) 1);
  by (blast_tac (claset() addDs [boundedD]) 1);
-by(stac nth_merges 1);
-     ba 1;
-    ba 1;
-   ba 2;
+by (stac nth_merges 1);
+     by (assume_tac 1);
+    by (assume_tac 1);
+   by (assume_tac 2);
   by (blast_tac (claset() addDs [boundedD]) 1);
  by (blast_tac (claset() addDs [boundedD]) 1);
 by (Simp_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
- by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
  by (blast_tac (claset() addSIs [semilat_ub1,semilat_ub2,listE_nth_in] addIs [order_trans]addDs [boundedD]) 1);
 by (blast_tac (claset() addSIs [semilat_ub1,semilat_ub2,listE_nth_in] addIs [order_trans]addDs [boundedD]) 1);
 qed "stable_pres_lemma";
@@ -289,43 +289,43 @@
 \     (! ts:list n A. \
 \          ss <=[r] ts & stables r step succs ts --> \
 \          iter(((A,r,f),step,succs),ss,w) <=[r] ts)";
-by(res_inst_tac [("A","A"),("r","r"),("f","f"),("step","step"),("ss","ss"),("w","w")]iter_induct 1);
-by(Clarify_tac 1);
-by(ftac listE_length 1);
-by(hyp_subst_tac 1);
-by(stac iter_unfold 1);
-      ba 1;
-     ba 1;
+by (res_inst_tac [("A","A"),("r","r"),("f","f"),("step","step"),("ss","ss"),("w","w")]iter_induct 1);
+by (Clarify_tac 1);
+by (ftac listE_length 1);
+by (hyp_subst_tac 1);
+by (stac iter_unfold 1);
+      by (assume_tac 1);
+     by (assume_tac 1);
     by (Asm_simp_tac 1);
-   ba 1;
-  ba 1;
- ba 1;
-by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
-br impI 1;
-be allE 1;
-be impE 1;
- by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
-by(subgoal_tac "(@p. p:w) : w" 1);
+   by (assume_tac 1);
+  by (assume_tac 1);
+ by (assume_tac 1);
+by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (rtac impI 1);
+by (etac allE 1);
+by (etac impE 1);
+ by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (subgoal_tac "(@p. p:w) : w" 1);
  by (fast_tac (claset() addIs [someI]) 2);
-by(subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
+by (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
  by (blast_tac (claset() addIs [pres_typeD,listE_nth_in]) 2);
-be impE 1;
- by(asm_simp_tac (simpset() delsimps [listE_length,le_iff_plus_unchanged RS sym]) 1);
- br conjI 1;
+by (etac impE 1);
+ by (asm_simp_tac (simpset() delsimps [listE_length,le_iff_plus_unchanged RS sym]) 1);
+ by (rtac conjI 1);
   by (blast_tac (claset() addDs [boundedD]) 1);
- br conjI 1;
-  by(blast_tac (claset() addIs[merges_preserves_type]addDs[boundedD]) 1);
+ by (rtac conjI 1);
+  by (blast_tac (claset() addIs[merges_preserves_type]addDs[boundedD]) 1);
  by (blast_tac (claset() addSIs [stable_pres_lemma]) 1);
-by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
-by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
+by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
  by (blast_tac (claset() addDs [boundedD]) 2);
-by(subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
+by (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
  by (blast_tac (claset() addIs [pres_typeD]) 2);
-br conjI 1;
+by (rtac conjI 1);
  by (blast_tac (claset() addSIs [merges_incr] addIs [le_list_trans]) 1);
-by(Clarify_tac 1);
-by(EVERY1[dtac bspec, atac, etac mp]);
-by(asm_full_simp_tac (simpset() delsimps [listE_length]) 1);
+by (Clarify_tac 1);
+by (EVERY1[dtac bspec, atac, etac mp]);
+by (asm_full_simp_tac (simpset() delsimps [listE_length]) 1);
 by (blast_tac (claset() addIs [merges_bounded_lemma]) 1);
 qed_spec_mp "iter_properties";
 
@@ -334,11 +334,11 @@
  "[| semilat(A,r,f); acc r; pres_type step n A; \
 \    mono r step n A; bounded succs n|] ==> \
 \ is_dfa r (kildall (A,r,f) step succs) step succs n A";
-by(Clarify_tac 1);
-by(Simp_tac 1);
-br iter_properties 1;
-by(asm_simp_tac (simpset() addsimps [unstables_def,stable_def]) 1);
-by(blast_tac (claset() addSIs [le_iff_plus_unchanged RS iffD2,listE_nth_in]
+by (Clarify_tac 1);
+by (Simp_tac 1);
+by (rtac iter_properties 1);
+by (asm_simp_tac (simpset() addsimps [unstables_def,stable_def]) 1);
+by (blast_tac (claset() addSIs [le_iff_plus_unchanged RS iffD2,listE_nth_in]
               addDs [boundedD,pres_typeD]) 1);
 qed "is_dfa_kildall";
 
diff -r 59d6633835fa -r 3daeda3d3cd0 src/HOL/BCV/Listn.ML
--- a/src/HOL/BCV/Listn.ML	Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Listn.ML	Mon Oct 09 12:23:45 2000 +0200
@@ -21,7 +21,7 @@
 AddIffs [Nil_le_conv,Cons_notle_Nil];
 
 Goalw [lesub_def,Listn.le_def] "x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "Cons_le_Cons";
 AddIffs [Cons_le_Cons];
 
@@ -34,7 +34,7 @@
 
 Goalw [unfold_lesub_list]
  "[| i<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]";
-by(rewtac Listn.le_def);
+by (rewtac Listn.le_def);
 by (asm_full_simp_tac (simpset() addsimps [list_all2_conv_all_nth,nth_list_update]) 1);
 qed "list_update_le_cong";
 
@@ -59,7 +59,7 @@
 Goalw [unfold_lesub_list]
  "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys";
 by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1);
-br nth_equalityI 1;
+by (rtac nth_equalityI 1);
  by (Blast_tac 1);
 by (Clarify_tac 1);
 by (Asm_full_simp_tac 1);
@@ -67,8 +67,8 @@
 qed "le_list_antisym";
 
 Goal "order r ==> order(Listn.le r)";
-by(stac order_def 1);
-by(blast_tac (claset() addIs [le_list_refl,le_list_trans,le_list_antisym]
+by (stac order_def 1);
+by (blast_tac (claset() addIs [le_list_refl,le_list_trans,le_list_antisym]
                        addDs [order_refl]) 1);
 qed "order_listI";
 Addsimps [order_listI];
@@ -81,11 +81,11 @@
 Addsimps [lesub_list_impl_same_size];
 
 Goalw [lesssub_def] "xs <_(Listn.le r) ys ==> size ys = size xs";
-by(Auto_tac);
+by (Auto_tac);
 qed "lesssub_list_impl_same_size";
 
 Goalw [list_def] "[| length xs = n; set xs <= A |] ==> xs : list n A";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "listI";
 
 Goalw [list_def] "xs : list n A ==> length xs = n";
@@ -94,7 +94,7 @@
 Addsimps [listE_length];
 
 Goal "[| xs : list n A; p < n |] ==> p < length xs";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "less_lengthI";
 
 Goalw [list_def] "xs : list n A ==> set xs <= A";
@@ -159,7 +159,7 @@
 Goal "!ys. length(xs +[f] ys) = min(length xs) (length ys)";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (asm_simp_tac (simpset() addsplits [list.split]) 1);
 qed_spec_mp "length_plus_list";
 Addsimps [length_plus_list];
@@ -208,23 +208,23 @@
 qed_spec_mp "list_update_incr";
 
 Goalw [acc_def] "[| order r; acc r |] ==> acc(Listn.le r)";
-by(subgoal_tac
+by (subgoal_tac
  "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})" 1);
- be wf_subset 1;
- by(blast_tac (claset() addIs [lesssub_list_impl_same_size]) 1);
-br wf_UN 1;
+ by (etac wf_subset 1);
+ by (blast_tac (claset() addIs [lesssub_list_impl_same_size]) 1);
+by (rtac wf_UN 1);
  by (Clarify_tac 2);
- by(rename_tac "m n" 2);
- by(case_tac "m=n" 2);
-  by(Asm_full_simp_tac 2);
- br conjI 2;
-  by(fast_tac (claset() addSIs [equals0I] addDs [not_sym]) 2);
- by(fast_tac (claset() addSIs [equals0I] addDs [not_sym]) 2);
+ by (rename_tac "m n" 2);
+ by (case_tac "m=n" 2);
+  by (Asm_full_simp_tac 2);
+ by (rtac conjI 2);
+  by (fast_tac (claset() addSIs [equals0I] addDs [not_sym]) 2);
+ by (fast_tac (claset() addSIs [equals0I] addDs [not_sym]) 2);
 by (Clarify_tac 1);
-by(rename_tac "n" 1);
+by (rename_tac "n" 1);
 by (induct_tac "n" 1);
  by (simp_tac (simpset() addsimps [lesssub_def] addcongs [conj_cong]) 1);
-by(rename_tac "k" 1);
+by (rename_tac "k" 1);
 by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
 by (simp_tac (simpset() addsimps [length_Suc_conv] addcongs [conj_cong]) 1);
 by (Clarify_tac 1);
@@ -240,53 +240,53 @@
 by (Clarify_tac 1);
 by (rename_tac "maxA xs" 1);
 by (eres_inst_tac [("x","{ys. size ys = size xs & maxA#ys : M}")] allE 1);
-be impE 1;
- by(Blast_tac 1);
+by (etac impE 1);
+ by (Blast_tac 1);
 by (Clarify_tac 1);
 by (thin_tac "m : M" 1);
 by (thin_tac "maxA#xs : M" 1);
 by (rtac bexI 1);
- ba 2;
+ by (assume_tac 2);
 by (Clarify_tac 1);
-by(Asm_full_simp_tac 1);
-by(Blast_tac 1);
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
 qed "acc_le_listI";
 AddSIs [acc_le_listI];
 
 
 Goalw [closed_def]
  "closed S f ==> closed (list n S) (map2 f)";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
-by(Simp_tac 1);
+by (Clarify_tac 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "closed_listI";
 
 
 Goalw [Listn.sl_def]
  "!!L. semilat L ==> semilat (Listn.sl n L)";
-by(split_all_tac 1);
-by(simp_tac (HOL_basic_ss addsimps [semilat_Def,split]) 1);
-br conjI 1;
- by(Asm_simp_tac 1);
-br conjI 1;
- by(asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_listI]) 1);
-by(simp_tac (HOL_basic_ss addsimps [list_def]) 1);
+by (split_all_tac 1);
+by (simp_tac (HOL_basic_ss addsimps [semilat_Def,split]) 1);
+by (rtac conjI 1);
+ by (Asm_simp_tac 1);
+by (rtac conjI 1);
+ by (asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_listI]) 1);
+by (simp_tac (HOL_basic_ss addsimps [list_def]) 1);
 by (asm_simp_tac (simpset() addsimps [plus_list_ub1,plus_list_ub2,plus_list_lub]) 1);
 qed "semilat_Listn_sl";
 
 
 Goal "!xes. xes : list n (err A) --> coalesce xes : err(list n A)";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (simp_tac (simpset() addsimps [plussub_def,Err.sup_def,lift2_def] addsplits [err.split]) 1);
-by(Force_tac 1);
+by (Force_tac 1);
 qed_spec_mp "coalesce_in_err_list";
 
 
@@ -298,37 +298,37 @@
  "semilat(err A, Err.le r, lift2 f) ==> \
 \ !xs. xs : list n A --> (!ys. ys : list n A --> \
 \      (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1);
-by(force_tac (claset(), simpset() addsimps [semilat_le_err_OK1]) 1);
+by (force_tac (claset(), simpset() addsimps [semilat_le_err_OK1]) 1);
 qed_spec_mp "coalesce_eq_OK1_D";
 
 Goal
  "semilat(err A, Err.le r, lift2 f) ==> \
 \ !xs. xs : list n A --> (!ys. ys : list n A --> \
 \      (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1);
-by(force_tac (claset(), simpset() addsimps [semilat_le_err_OK2]) 1);
+by (force_tac (claset(), simpset() addsimps [semilat_le_err_OK2]) 1);
 qed_spec_mp "coalesce_eq_OK2_D";
 
 Goalw [semilat_Def,plussub_def,err_def]
  "[| semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; \
 \    u:A; x <=_r u; y <=_r u |] ==> z <=_r u";
-by(asm_full_simp_tac (simpset() addsimps [lift2_def]) 1);
-by(Clarify_tac 1);
-by(rotate_tac ~3 1);
-by(etac thin_rl 1);
-by(etac thin_rl 1);
-by(Force_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [lift2_def]) 1);
+by (Clarify_tac 1);
+by (rotate_tac ~3 1);
+by (etac thin_rl 1);
+by (etac thin_rl 1);
+by (Force_tac 1);
 qed "lift2_le_ub";
 
 Goal
@@ -336,22 +336,22 @@
 \ !xs. xs : list n A --> (!ys. ys : list n A --> \
 \      (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us \
 \               & us : list n A --> zs <=[r] us))";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1);
-by(Clarify_tac 1);
-br conjI 1;
- by(Blast_tac 2);
-by(blast_tac (claset() addIs [lift2_le_ub]) 1);
+by (Clarify_tac 1);
+by (rtac conjI 1);
+ by (Blast_tac 2);
+by (blast_tac (claset() addIs [lift2_le_ub]) 1);
 qed_spec_mp "coalesce_eq_OK_ub_D";
 
 Goal
  "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A |] \
 \ ==> ~(? u:A. x <=_r u & y <=_r u)";
-by(asm_simp_tac (simpset() addsimps [OK_plus_OK_eq_Err_conv RS iffD1]) 1);
+by (asm_simp_tac (simpset() addsimps [OK_plus_OK_eq_Err_conv RS iffD1]) 1);
 qed "lift2_eq_ErrD";
 
 Goal
@@ -359,39 +359,39 @@
 \ |] ==> !xs. xs:list n A --> (!ys. ys:list n A --> \
 \  coalesce (xs +[f] ys) = Err --> \
 \ ~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1);
- by(blast_tac (claset() addDs [lift2_eq_ErrD]) 1);
-by(Blast_tac 1);
+ by (blast_tac (claset() addDs [lift2_eq_ErrD]) 1);
+by (Blast_tac 1);
 qed_spec_mp "coalesce_eq_Err_D";
 
 
 Goalw [closed_def]
  "closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)";
-by(simp_tac (simpset() addsimps [err_def]) 1);
+by (simp_tac (simpset() addsimps [err_def]) 1);
 qed "closed_err_lift2_conv";
 
 Goalw [map2_def]
  "closed (err A) (lift2 f) ==> \
 \ !xs. xs : list n A --> (!ys. ys : list n A --> \
 \     map2 f xs ys : list n (err A))";
-by(induct_tac "n" 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsimps [plussub_def,closed_err_lift2_conv]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "closed_map2_list";
 
 Goal
  "closed (err A) (lift2 f) ==> \
 \ closed (err (list n A)) (lift2 (sup f))";
-by(fast_tac (claset() addss (simpset() addsimps
+by (fast_tac (claset() addss (simpset() addsimps
  [closed_def,plussub_def,sup_def,lift2_def,
   coalesce_in_err_list,closed_map2_list]
  addsplits [err.split])) 1);
@@ -400,24 +400,24 @@
 Goalw [Err.sl_def]
  "err_semilat (A,r,f) ==> \
 \ err_semilat (list n A, Listn.le r, sup f)";
-by(asm_full_simp_tac (HOL_basic_ss addsimps [split]) 1);
-by(simp_tac (HOL_basic_ss addsimps [semilat_Def,plussub_def]) 1);
-by(asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_lift2_sup]) 1);
-br conjI 1;
- bd semilatDorderI 1;
- by(Asm_full_simp_tac 1);
-by(simp_tac (HOL_basic_ss addsimps
+by (asm_full_simp_tac (HOL_basic_ss addsimps [split]) 1);
+by (simp_tac (HOL_basic_ss addsimps [semilat_Def,plussub_def]) 1);
+by (asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_lift2_sup]) 1);
+by (rtac conjI 1);
+ by (dtac semilatDorderI 1);
+ by (Asm_full_simp_tac 1);
+by (simp_tac (HOL_basic_ss addsimps
      [unfold_lesub_err,Err.le_def,err_def,sup_def,lift2_def]) 1);
 by (asm_simp_tac (simpset() addsimps
      [coalesce_eq_OK1_D,coalesce_eq_OK2_D] addsplits [err.split]) 1);
-by(blast_tac (claset()addIs[coalesce_eq_OK_ub_D] addDs [coalesce_eq_Err_D]) 1);
+by (blast_tac (claset()addIs[coalesce_eq_OK_ub_D] addDs [coalesce_eq_Err_D]) 1);
 qed "err_semilat_sup";
 
 Goalw [Listn.upto_esl_def]
  "!!L. err_semilat L ==> err_semilat(upto_esl m L)";
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
-by(fast_tac (claset()
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac (claset()
   addSIs [err_semilat_UnionI,err_semilat_sup]
   addDs [lesub_list_impl_same_size] addss (simpset()
   addsimps [plussub_def,Listn.sup_def])) 1);
diff -r 59d6633835fa -r 3daeda3d3cd0 src/HOL/BCV/Opt.ML
--- a/src/HOL/BCV/Opt.ML	Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Opt.ML	Mon Oct 09 12:23:45 2000 +0200
@@ -8,7 +8,7 @@
  "o1 <=_(le r) o2 = \
 \ (case o2 of None => o1=None | \
 \             Some y => (case o1 of None => True | Some x => x <=_r y))";
-br refl 1;
+by (rtac refl 1);
 qed "unfold_le_opt";
 
 Goal "order r ==> o1 <=_(le r) o1";
@@ -27,32 +27,32 @@
 qed_spec_mp "le_opt_antisym";
 
 Goal "order r ==> order(le r)";
-by(stac order_def 1);
-by(blast_tac (claset() addIs [le_opt_refl,le_opt_trans,le_opt_antisym]) 1);
+by (stac order_def 1);
+by (blast_tac (claset() addIs [le_opt_refl,le_opt_trans,le_opt_antisym]) 1);
 qed "order_le_opt";
 AddSIs [order_le_opt];
 Addsimps [order_le_opt];
 
 Goalw [lesub_def,le_def] "None <=_(le r) ox";
-by(simp_tac (simpset() addsplits [option.split]) 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
 qed "None_bot";
 AddIffs [None_bot];
 
 Goalw [lesub_def,le_def]
  "(Some x <=_(le r) ox) = (? y. ox = Some y & x <=_r y)";
-by(simp_tac (simpset() addsplits [option.split]) 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
 qed "Some_le";
 AddIffs [Some_le];
 
 Goalw [lesub_def,le_def] "(ox <=_(le r) None) = (ox = None)";
-by(simp_tac (simpset() addsplits [option.split]) 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
 qed "le_None";
 AddIffs [le_None];
 
 
 Goalw [Opt.sl_def,semilat_def,closed_def,split RS eq_reflection]
  "!!L. semilat L ==> semilat (Opt.sl L)";
-by(split_all_tac 1);
+by (split_all_tac 1);
 by (asm_full_simp_tac (simpset() addsplits [option.split]
  addsimps [lesub_def,Opt.le_def,plussub_def,Opt.sup_def,opt_def,Bex_def]) 1);
 by (asm_full_simp_tac (simpset() addsimps [order_def,lesub_def]) 1);
@@ -60,16 +60,16 @@
 
 
 Goalw [top_def] "top (le r) (Some T) = top r T";
-br iffI 1;
- by(Blast_tac 1);
-br allI 1;
-by(case_tac "x" 1);
-by(ALLGOALS Asm_simp_tac);
+by (rtac iffI 1);
+ by (Blast_tac 1);
+by (rtac allI 1);
+by (case_tac "x" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "top_le_opt_Some";
 AddIffs [top_le_opt_Some];
 
 Goalw [top_def] "[| order r; top r T |] ==> (T <=_r x) = (x = T)";
-by(blast_tac (claset() addIs [order_antisym]) 1);
+by (blast_tac (claset() addIs [order_antisym]) 1);
 qed "Top_le_conv";
 
 
@@ -100,6 +100,6 @@
  "[| ox : opt S; !x:S. ox = Some x --> f x : S |] \
 \ ==> option_map f ox : opt S";
 by (asm_simp_tac (simpset() addsplits [option.split]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "option_map_in_optionI";
 
diff -r 59d6633835fa -r 3daeda3d3cd0 src/HOL/BCV/Product.ML
--- a/src/HOL/BCV/Product.ML	Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Product.ML	Mon Oct 09 12:23:45 2000 +0200
@@ -10,29 +10,29 @@
 
 Goalw [lesub_def,le_def]
  "((a1,b1) <=(rA,rB) (a2,b2)) = (a1 <=_rA a2 & b1 <=_rB b2)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "le_prod_Pair_conv";
 AddIffs [le_prod_Pair_conv];
 
 Goalw [lesssub_def]
  "((a1,b1) <_(Product.le rA rB) (a2,b2)) = \
 \ (a1 <_rA a2 & b1 <=_rB b2 | a1 <=_rA a2 & b1 <_rB b2)";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 qed "less_prod_Pair_conv";
 
 Goalw [order_def] "order(Product.le rA rB) = (order rA & order rB)";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 qed "order_le_prod";
 AddIffs [order_le_prod];
 
 
 Goalw [acc_def] "[| acc rA; acc rB |] ==> acc(Product.le rA rB)";
-br wf_subset 1;
- be wf_lex_prod 1;
- ba 1;
-by(auto_tac (claset(), simpset()
+by (rtac wf_subset 1);
+ by (etac wf_lex_prod 1);
+ by (assume_tac 1);
+by (auto_tac (claset(), simpset()
      addsimps [lesssub_def,less_prod_Pair_conv,lex_prod_def]));
 qed "acc_le_prodI";
 AddSIs [acc_le_prodI];
@@ -41,8 +41,8 @@
 Goalw [closed_def,plussub_def,lift2_def,err_def,sup_def]
  "[| closed (err A) (lift2 f); closed (err B) (lift2 g) |] ==> \
 \ closed (err(A<*>B)) (lift2(sup f g))";
-by(asm_full_simp_tac (simpset() addsplits [err.split]) 1);
-by(Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [err.split]) 1);
+by (Blast_tac 1);
 qed "closed_lift2_sup";
 
 Goalw [plussub_def] "e1 +_(lift2 f) e2 == lift2 f e1 e2";
@@ -52,63 +52,63 @@
 Goal
  "[| x:A; y:A; semilat(err A, Err.le r, lift2 f) |] ==> \
 \ (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))";
-br iffI 1;
+by (rtac iffI 1);
  by (Clarify_tac 1);
- bd (OK_le_err_OK RS iffD2) 1;
- bd (OK_le_err_OK RS iffD2) 1;
- bd semilat_lub 1;
-      ba 1;
-     ba 1;
-    by(Asm_simp_tac 1); 
-   by(Asm_simp_tac 1); 
-  by(Asm_simp_tac 1); 
- by(Asm_full_simp_tac 1);
-by(case_tac "x +_f y" 1);
- ba 1;
-by(rename_tac "z" 1);
-by(subgoal_tac "OK z: err A" 1);
- by(ftac (rotate_prems 2 (read_instantiate_sg(sign_of Err.thy)[("x","OK(x::'a)"),("y","OK(y::'a)")]plus_le_conv RS iffD1))1);
-     ba 1;
-    by(Asm_simp_tac 1); 
-    by(blast_tac (claset() addDs [semilatDorderI,order_refl]) 1);
-   by(Asm_simp_tac 1); 
-  by(Asm_simp_tac 1);
- by(Blast_tac 1);
-by(etac subst 1);
-by(rewrite_goals_tac [semilat_def,err_def,closed_def]);
-by(Asm_full_simp_tac 1);
+ by (dtac (OK_le_err_OK RS iffD2) 1);
+ by (dtac (OK_le_err_OK RS iffD2) 1);
+ by (dtac semilat_lub 1);
+      by (assume_tac 1);
+     by (assume_tac 1);
+    by (Asm_simp_tac 1); 
+   by (Asm_simp_tac 1); 
+  by (Asm_simp_tac 1); 
+ by (Asm_full_simp_tac 1);
+by (case_tac "x +_f y" 1);
+ by (assume_tac 1);
+by (rename_tac "z" 1);
+by (subgoal_tac "OK z: err A" 1);
+ by (ftac (rotate_prems 2 (read_instantiate_sg(sign_of Err.thy)[("x","OK(x::'a)"),("y","OK(y::'a)")]plus_le_conv RS iffD1))1);
+     by (assume_tac 1);
+    by (Asm_simp_tac 1); 
+    by (blast_tac (claset() addDs [semilatDorderI,order_refl]) 1);
+   by (Asm_simp_tac 1); 
+  by (Asm_simp_tac 1);
+ by (Blast_tac 1);
+by (etac subst 1);
+by (rewrite_goals_tac [semilat_def,err_def,closed_def]);
+by (Asm_full_simp_tac 1);
 qed "plus_eq_Err_conv";
 Addsimps [plus_eq_Err_conv];
 
 Goalw [esl_def,Err.sl_def]
  "!!L1 L2. [| err_semilat L1; err_semilat L2 |] ==> err_semilat(Product.esl L1 L2)";
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
-by(simp_tac (HOL_basic_ss addsimps [semilat_Def]) 1);
-by(asm_simp_tac(HOL_basic_ss addsimps[semilatDclosedI,closed_lift2_sup])1);
-by(simp_tac (HOL_basic_ss addsimps
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
+by (simp_tac (HOL_basic_ss addsimps [semilat_Def]) 1);
+by (asm_simp_tac(HOL_basic_ss addsimps[semilatDclosedI,closed_lift2_sup])1);
+by (simp_tac (HOL_basic_ss addsimps
      [unfold_lesub_err,Err.le_def,unfold_plussub_lift2,sup_def]) 1);
 by (auto_tac (claset() addEs [semilat_le_err_OK1,semilat_le_err_OK2],
       simpset() addsimps [lift2_def] addsplits [err.split]));
-by(blast_tac (claset() addDs [semilatDorderI]) 1);
-by(blast_tac (claset() addDs [semilatDorderI]) 1);
+by (blast_tac (claset() addDs [semilatDorderI]) 1);
+by (blast_tac (claset() addDs [semilatDorderI]) 1);
 
-br (OK_le_err_OK RS iffD1) 1;
-by(etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
+by (rtac (OK_le_err_OK RS iffD1) 1);
+by (etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 
-br (OK_le_err_OK RS iffD1) 1;
-by(etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
-by(Asm_simp_tac 1);
+by (rtac (OK_le_err_OK RS iffD1) 1);
+by (etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 
 qed "err_semilat_Product_esl";
diff -r 59d6633835fa -r 3daeda3d3cd0 src/HOL/BCV/Semilat.ML
--- a/src/HOL/BCV/Semilat.ML	Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Semilat.ML	Mon Oct 09 12:23:45 2000 +0200
@@ -5,37 +5,37 @@
 *)
 
 Goalw [order_def] "order r ==> x <=_r x";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "order_refl";
 Addsimps [order_refl];
 AddIs [order_refl];
 
 Goalw [order_def] "[| order r; x <=_r y; y <=_r x |] ==> x = y";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "order_antisym";
 
 Goalw [order_def] "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "order_trans";
 
 Goalw [order_def,lesssub_def] "order r ==> ~ x <_r x";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "order_less_irrefl";
 AddIs [order_less_irrefl];
 Addsimps [order_less_irrefl];
 
 Goalw [order_def,lesssub_def] "[| order r; x <_r y; y <_r z |] ==> x <_r z";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "order_less_trans";
 
 Goalw [top_def] "top r T ==> x <=_r T";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "topD";
 Addsimps [topD];
 AddIs [topD];
 
 Goal "[| order r; top r T |] ==> (T <=_r x) = (x = T)";
-by(blast_tac (claset() addIs [order_antisym]) 1);
+by (blast_tac (claset() addIs [order_antisym]) 1);
 qed "top_le_conv";
 Addsimps [top_le_conv];
 
@@ -44,32 +44,32 @@
 \                (!x:A. !y:A. x <=_r x +_f y)  & \
 \                (!x:A. !y:A. y <=_r x +_f y)  & \
 \                (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)";
-br (refl RS eq_reflection) 1;
+by (rtac (refl RS eq_reflection) 1);
 qed "semilat_Def";
 
 Goalw [semilat_Def] "semilat(A,r,f) ==> order r";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "semilatDorderI";
 Addsimps [semilatDorderI];
 AddIs [semilatDorderI];
 
 Goalw [semilat_Def] "semilat(A,r,f) ==> closed A f";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "semilatDclosedI";
 Addsimps [semilatDclosedI];
 AddIs [semilatDclosedI];
 
 Goalw [semilat_Def] "[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "semilat_ub1";
 
 Goalw [semilat_Def] "[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "semilat_ub2";
 
 Goalw [semilat_Def]
  "[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "semilat_lub";
 
 Addsimps [semilat_ub1,semilat_ub2,semilat_lub];
@@ -98,11 +98,11 @@
 (*** closed ***)
 
 Goalw [closed_def] "[| closed A f; x:A; y:A |] ==> x +_f y : A";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "closedD";
 
 Goalw [closed_def] "closed UNIV f";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "closed_UNIV";
 AddIffs [closed_UNIV];
 
@@ -110,17 +110,17 @@
 
 Goalw [is_lub_def]
  "is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)";
-ba 1;
+by (assume_tac 1);
 qed "is_lubD";
 
 Goalw [is_ub_def]
  "[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "is_ubI";
 
 Goalw [is_ub_def]
  "is_ub r x y u ==> (x,u) : r & (y,u) : r";
-ba 1;
+by (assume_tac 1);
 qed "is_ubD";
 
 
@@ -138,40 +138,40 @@
 Goalw [is_lub_def,is_ub_def]
  "[| univalent r; is_lub (r^*) x y u; (x',x) : r |] ==> \
 \    EX v. is_lub (r^*) x' y v";
-by(case_tac "(y,x) : r^*" 1);
- by(case_tac "(y,x') : r^*" 1);
+by (case_tac "(y,x) : r^*" 1);
+ by (case_tac "(y,x') : r^*" 1);
   by (Blast_tac 1);
- by(blast_tac (claset() addIs [r_into_rtrancl] addEs [converse_rtranclE]
+ by (blast_tac (claset() addIs [r_into_rtrancl] addEs [converse_rtranclE]
                         addDs [univalentD]) 1);
-br exI 1;
-br conjI 1;
- by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [univalentD]) 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl,rtrancl_into_rtrancl2]
+by (rtac exI 1);
+by (rtac conjI 1);
+ by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [univalentD]) 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl,rtrancl_into_rtrancl2]
                        addEs [converse_rtranclE] addDs [univalentD]) 1);
 qed "extend_lub";
 
 Goal "[| univalent r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> \
 \     (EX z. is_lub (r^*) x y z))";
-by(etac converse_rtrancl_induct 1);
- by(Clarify_tac 1);
- by(etac converse_rtrancl_induct 1);
-  by(Blast_tac 1);
- by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
-by(blast_tac (claset() addIs [extend_lub]) 1);
+by (etac converse_rtrancl_induct 1);
+ by (Clarify_tac 1);
+ by (etac converse_rtrancl_induct 1);
+  by (Blast_tac 1);
+ by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
+by (blast_tac (claset() addIs [extend_lub]) 1);
 qed_spec_mp "univalent_has_lubs";
 
 Goalw [some_lub_def,is_lub_def]
  "[| acyclic r; is_lub (r^*) x y u |] ==> some_lub (r^*) x y = u";
-br someI2 1;
- ba 1;
-by(blast_tac (claset() addIs [antisymD]
+by (rtac someI2 1);
+ by (assume_tac 1);
+by (blast_tac (claset() addIs [antisymD]
                        addSDs [acyclic_impl_antisym_rtrancl]) 1);
 qed "some_lub_conv";
 
 Goal
  "[| univalent r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> \
 \ is_lub (r^*) x y (some_lub (r^*) x y)";
-by(fast_tac
+by (fast_tac
     (claset() addDs [univalent_has_lubs]
      addss (simpset() addsimps [some_lub_conv])) 1);
 qed "is_lub_some_lub";