--- a/src/HOL/Integ/Group.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/Integ/Group.ML Wed Apr 23 11:02:19 1997 +0200
@@ -9,78 +9,78 @@
Addsimps [zeroL,zeroR,plus_assoc,plus_commute];
goal Group.thy "!!x::'a::add_group. (zero-x)+(x+y) = y";
-br trans 1;
-br (plus_assoc RS sym) 1;
-by(stac left_inv 1);
-br zeroL 1;
+by (rtac trans 1);
+by (rtac (plus_assoc RS sym) 1);
+by (stac left_inv 1);
+by (rtac zeroL 1);
qed "left_inv2";
goal Group.thy "!!x::'a::add_group. (zero-(zero-x)) = x";
-br trans 1;
-by(res_inst_tac [("x","zero-x")] left_inv2 2);
-by(stac left_inv 1);
-br (zeroR RS sym) 1;
+by (rtac trans 1);
+by (res_inst_tac [("x","zero-x")] left_inv2 2);
+by (stac left_inv 1);
+by (rtac (zeroR RS sym) 1);
qed "inv_inv";
goal Group.thy "zero-zero = (zero::'a::add_group)";
-br trans 1;
-br (zeroR RS sym) 1;
-br trans 1;
-by(res_inst_tac [("x","zero")] left_inv2 2);
-by(Simp_tac 1);
+by (rtac trans 1);
+by (rtac (zeroR RS sym) 1);
+by (rtac trans 1);
+by (res_inst_tac [("x","zero")] left_inv2 2);
+by (Simp_tac 1);
qed "inv_zero";
goal Group.thy "!!x::'a::add_group. x+(zero-x) = zero";
-br trans 1;
-by(res_inst_tac [("x","zero-x")] left_inv 2);
-by(stac inv_inv 1);
-br refl 1;
+by (rtac trans 1);
+by (res_inst_tac [("x","zero-x")] left_inv 2);
+by (stac inv_inv 1);
+by (rtac refl 1);
qed "right_inv";
goal Group.thy "!!x::'a::add_group. x+((zero-x)+y) = y";
-br trans 1;
-by(res_inst_tac [("x","zero-x")] left_inv2 2);
-by(stac inv_inv 1);
-br refl 1;
+by (rtac trans 1);
+by (res_inst_tac [("x","zero-x")] left_inv2 2);
+by (stac inv_inv 1);
+by (rtac refl 1);
qed "right_inv2";
goal Group.thy "!!x::'a::add_group. x-x = zero";
-by(stac minus_inv 1);
-br right_inv 1;
+by (stac minus_inv 1);
+by (rtac right_inv 1);
qed "minus_self_zero";
Addsimps [minus_self_zero];
goal Group.thy "!!x::'a::add_group. x-zero = x";
-by(stac minus_inv 1);
-by(stac inv_zero 1);
-br zeroR 1;
+by (stac minus_inv 1);
+by (stac inv_zero 1);
+by (rtac zeroR 1);
qed "minus_zero";
Addsimps [minus_zero];
val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
goal Group.thy "!!x::'a::add_group. zero-(x+y) = (zero-y)+(zero-x)";
-br trans 1;
- br zeroR 2;
-br trans 1;
- br plus_cong 2;
- br refl 2;
- by(res_inst_tac [("x","x+y")] right_inv 2);
-br trans 1;
- br plus_assoc 2;
-br trans 1;
- br plus_cong 2;
- by(simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
- br refl 2;
-br (zeroL RS sym) 1;
+by (rtac trans 1);
+ by (rtac zeroR 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 2);
+ by (res_inst_tac [("x","x+y")] right_inv 2);
+by (rtac trans 1);
+ by (rtac plus_assoc 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
+ by (rtac refl 2);
+by (rtac (zeroL RS sym) 1);
qed "inv_plus";
goal Group.thy "x+(y+z)=y+(x+z::'a::add_agroup)";
-br trans 1;
-br plus_commute 1;
-br trans 1;
-br plus_assoc 1;
-by(Simp_tac 1);
+by (rtac trans 1);
+by (rtac plus_commute 1);
+by (rtac trans 1);
+by (rtac plus_assoc 1);
+by (Simp_tac 1);
qed "plus_commuteL";
Addsimps [plus_commuteL];
@@ -89,39 +89,39 @@
(* Phase 1 *)
goal Group.thy "!!x::'a::add_agroup. (x+(zero-y))+z = (x+z)+(zero-y)";
-by(Simp_tac 1);
+by (Simp_tac 1);
val lemma = result();
bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+z)) = (x+(zero-y))+(zero-z)";
-by(Simp_tac 1);
+by (Simp_tac 1);
val lemma = result();
bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+(zero-z))) = (x+z)+(zero-y)";
-by(Simp_tac 1);
+by (Simp_tac 1);
val lemma = result();
bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
goal Group.thy "!!x::'a::add_agroup. x+(y+(zero-z)) = (x+y)+(zero-z)";
-by(Simp_tac 1);
+by (Simp_tac 1);
val lemma = result();
bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
(* Phase 2 *)
goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-z) = x+(y+(zero-z))";
-by(Simp_tac 1);
+by (Simp_tac 1);
val lemma = result();
bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-x) = y";
-br (plus_assoc RS trans) 1;
-br trans 1;
- br plus_cong 1;
- br refl 1;
- br right_inv2 2;
-br plus_commute 1;
+by (rtac (plus_assoc RS trans) 1);
+by (rtac trans 1);
+ by (rtac plus_cong 1);
+ by (rtac refl 1);
+ by (rtac right_inv2 2);
+by (rtac plus_commute 1);
val lemma = result();
bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
--- a/src/HOL/Integ/IntRing.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/Integ/IntRing.ML Wed Apr 23 11:02:19 1997 +0200
@@ -14,5 +14,5 @@
\ sq(i1*j2 + i2*j1 + i3*j4 - i4*j3) + \
\ sq(i1*j3 - i2*j4 + i3*j1 + i4*j2) + \
\ sq(i1*j4 + i2*j3 - i3*j2 + i4*j1)";
-br Lagrange_lemma 1;
+by (rtac Lagrange_lemma 1);
qed "Lagrange_lemma_int";
--- a/src/HOL/Integ/Ring.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/Integ/Ring.ML Wed Apr 23 11:02:19 1997 +0200
@@ -17,123 +17,123 @@
Addsimps [times_assoc,times_commute,distribL,distribR];
goal Ring.thy "!!x::'a::cring. x*(y*z)=y*(x*z)";
-br trans 1;
-br times_commute 1;
-br trans 1;
-br times_assoc 1;
-by(Simp_tac 1);
+by (rtac trans 1);
+by (rtac times_commute 1);
+by (rtac trans 1);
+by (rtac times_assoc 1);
+by (Simp_tac 1);
qed "times_commuteL";
Addsimps [times_commuteL];
val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
goal Ring.thy "!!x::'a::ring. zero*x = zero";
-br trans 1;
- br right_inv 2;
-br trans 1;
- br plus_cong 2;
- br refl 3;
- br trans 2;
- br times_cong 3;
- br zeroL 3;
- br refl 3;
- br (distribR RS sym) 2;
-br trans 1;
+by (rtac trans 1);
+ by (rtac right_inv 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 3);
+ by (rtac trans 2);
+ by (rtac times_cong 3);
+ by (rtac zeroL 3);
+ by (rtac refl 3);
+ by (rtac (distribR RS sym) 2);
+by (rtac trans 1);
br(plus_assoc RS sym) 2;
-br trans 1;
- br plus_cong 2;
- br refl 2;
- br (right_inv RS sym) 2;
-br (zeroR RS sym) 1;
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 2);
+ by (rtac (right_inv RS sym) 2);
+by (rtac (zeroR RS sym) 1);
qed "mult_zeroL";
goal Ring.thy "!!x::'a::ring. x*zero = zero";
-br trans 1;
- br right_inv 2;
-br trans 1;
- br plus_cong 2;
- br refl 3;
- br trans 2;
- br times_cong 3;
- br zeroL 4;
- br refl 3;
- br (distribL RS sym) 2;
-br trans 1;
+by (rtac trans 1);
+ by (rtac right_inv 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 3);
+ by (rtac trans 2);
+ by (rtac times_cong 3);
+ by (rtac zeroL 4);
+ by (rtac refl 3);
+ by (rtac (distribL RS sym) 2);
+by (rtac trans 1);
br(plus_assoc RS sym) 2;
-br trans 1;
- br plus_cong 2;
- br refl 2;
- br (right_inv RS sym) 2;
-br (zeroR RS sym) 1;
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 2);
+ by (rtac (right_inv RS sym) 2);
+by (rtac (zeroR RS sym) 1);
qed "mult_zeroR";
goal Ring.thy "!!x::'a::ring. (zero-x)*y = zero-(x*y)";
-br trans 1;
- br zeroL 2;
-br trans 1;
- br plus_cong 2;
- br refl 3;
- br mult_zeroL 2;
-br trans 1;
- br plus_cong 2;
- br refl 3;
- br times_cong 2;
- br left_inv 2;
- br refl 2;
-br trans 1;
- br plus_cong 2;
- br refl 3;
- br (distribR RS sym) 2;
-br trans 1;
+by (rtac trans 1);
+ by (rtac zeroL 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 3);
+ by (rtac mult_zeroL 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 3);
+ by (rtac times_cong 2);
+ by (rtac left_inv 2);
+ by (rtac refl 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 3);
+ by (rtac (distribR RS sym) 2);
+by (rtac trans 1);
br(plus_assoc RS sym) 2;
-br trans 1;
- br plus_cong 2;
- br refl 2;
- br (right_inv RS sym) 2;
-br (zeroR RS sym) 1;
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 2);
+ by (rtac (right_inv RS sym) 2);
+by (rtac (zeroR RS sym) 1);
qed "mult_invL";
goal Ring.thy "!!x::'a::ring. x*(zero-y) = zero-(x*y)";
-br trans 1;
- br zeroL 2;
-br trans 1;
- br plus_cong 2;
- br refl 3;
- br mult_zeroR 2;
-br trans 1;
- br plus_cong 2;
- br refl 3;
- br times_cong 2;
- br refl 2;
- br left_inv 2;
-br trans 1;
- br plus_cong 2;
- br refl 3;
- br (distribL RS sym) 2;
-br trans 1;
+by (rtac trans 1);
+ by (rtac zeroL 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 3);
+ by (rtac mult_zeroR 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 3);
+ by (rtac times_cong 2);
+ by (rtac refl 2);
+ by (rtac left_inv 2);
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 3);
+ by (rtac (distribL RS sym) 2);
+by (rtac trans 1);
br(plus_assoc RS sym) 2;
-br trans 1;
- br plus_cong 2;
- br refl 2;
- br (right_inv RS sym) 2;
-br (zeroR RS sym) 1;
+by (rtac trans 1);
+ by (rtac plus_cong 2);
+ by (rtac refl 2);
+ by (rtac (right_inv RS sym) 2);
+by (rtac (zeroR RS sym) 1);
qed "mult_invR";
Addsimps[mult_invL,mult_invR];
goal Ring.thy "!!x::'a::ring. x*(y-z) = x*y - x*z";
-by(stac minus_inv 1);
-br sym 1;
-by(stac minus_inv 1);
-by(Simp_tac 1);
+by (stac minus_inv 1);
+by (rtac sym 1);
+by (stac minus_inv 1);
+by (Simp_tac 1);
qed "minus_distribL";
goal Ring.thy "!!x::'a::ring. (x-y)*z = x*z - y*z";
-by(stac minus_inv 1);
-br sym 1;
-by(stac minus_inv 1);
-by(Simp_tac 1);
+by (stac minus_inv 1);
+by (rtac sym 1);
+by (stac minus_inv 1);
+by (Simp_tac 1);
qed "minus_distribR";
Addsimps [minus_distribL,minus_distribR];
--- a/src/HOL/MiniML/Generalize.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/MiniML/Generalize.ML Wed Apr 23 11:02:19 1997 +0200
@@ -87,31 +87,31 @@
qed_spec_mp "gen_subst_commutes";
goal Generalize.thy "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
-by(typ.induct_tac "t" 1);
-by(ALLGOALS Asm_simp_tac);
-by(Fast_tac 1);
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+by (Fast_tac 1);
qed_spec_mp "bound_typ_inst_gen";
Addsimps [bound_typ_inst_gen];
goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
"gen ($ S A) ($ S t) <= $ S (gen A t)";
-by(safe_tac (!claset));
-by(rename_tac "R" 1);
-by(res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
-by(typ.induct_tac "t" 1);
- by(simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Asm_simp_tac 1);
+by (safe_tac (!claset));
+by (rename_tac "R" 1);
+by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
+by (typ.induct_tac "t" 1);
+ by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (Asm_simp_tac 1);
qed "gen_bound_typ_instance";
goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
"!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t";
-by(safe_tac (!claset));
-by(rename_tac "S" 1);
-by(res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
+by (safe_tac (!claset));
+by (rename_tac "S" 1);
+by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
by (typ.induct_tac "t" 1);
- by(asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
- by(Fast_tac 1);
-by(Asm_simp_tac 1);
+ by (asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+ by (Fast_tac 1);
+by (Asm_simp_tac 1);
qed "free_tv_subset_gen_le";
goalw thy [le_type_scheme_def,is_bound_typ_instance]
@@ -127,7 +127,7 @@
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (subgoal_tac "n <= n + nat" 1);
by (forw_inst_tac [("t","A")] new_tv_le 1);
-ba 1;
+by (assume_tac 1);
by (dtac new_tv_not_free_tv 1);
by (dtac new_tv_not_free_tv 1);
by (asm_simp_tac (!simpset addsimps [diff_add_inverse]) 1);
--- a/src/HOL/MiniML/Instance.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/MiniML/Instance.ML Wed Apr 23 11:02:19 1997 +0200
@@ -70,7 +70,7 @@
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (strip_tac 1);
by (dres_inst_tac [("x","x")] bspec 1);
-ba 1;
+by (assume_tac 1);
by (dres_inst_tac [("x","x")] bspec 1);
by (Asm_simp_tac 1);
by (Asm_full_simp_tac 1);
@@ -110,7 +110,7 @@
by (cut_inst_tac [("sch","sch")] fresh_variable_type_schemes 1);
by (cut_inst_tac [("sch","sch'")] fresh_variable_type_schemes 1);
by (dtac make_one_new_out_of_two 1);
-ba 1;
+by (assume_tac 1);
by (thin_tac "? n. new_tv n sch'" 1);
by (etac exE 1);
by (etac allE 1);
@@ -142,7 +142,7 @@
by (Asm_full_simp_tac 1);
by (rotate_tac 1 1);
by (rtac mp 1);
-ba 2;
+by (assume_tac 2);
by (type_scheme.induct_tac "sch" 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
@@ -160,18 +160,18 @@
goalw thy [le_env_def]
"(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)";
-by(Simp_tac 1);
-br iffI 1;
- by(SELECT_GOAL(safe_tac (!claset))1);
- by(eres_inst_tac [("x","0")] allE 1);
- by(Asm_full_simp_tac 1);
- by(eres_inst_tac [("x","Suc i")] allE 1);
- by(Asm_full_simp_tac 1);
-br conjI 1;
- by(Fast_tac 1);
-br allI 1;
-by(nat_ind_tac "i" 1);
-by(ALLGOALS Asm_simp_tac);
+by (Simp_tac 1);
+by (rtac iffI 1);
+ by (SELECT_GOAL(safe_tac (!claset))1);
+ by (eres_inst_tac [("x","0")] allE 1);
+ by (Asm_full_simp_tac 1);
+ by (eres_inst_tac [("x","Suc i")] allE 1);
+ by (Asm_full_simp_tac 1);
+by (rtac conjI 1);
+ by (Fast_tac 1);
+by (rtac allI 1);
+by (nat_ind_tac "i" 1);
+by (ALLGOALS Asm_simp_tac);
qed "le_env_Cons";
AddIffs [le_env_Cons];
@@ -196,59 +196,59 @@
qed "S_compatible_le_scheme_lists";
goalw thy [le_type_scheme_def] "!!t.[| t <| sch; sch <= sch' |] ==> t <| sch'";
-by(Fast_tac 1);
+by (Fast_tac 1);
qed "bound_typ_instance_trans";
goalw thy [le_type_scheme_def] "sch <= (sch::type_scheme)";
-by(Fast_tac 1);
+by (Fast_tac 1);
qed "le_type_scheme_refl";
AddIffs [le_type_scheme_refl];
goalw thy [le_env_def] "A <= (A::type_scheme list)";
-by(Fast_tac 1);
+by (Fast_tac 1);
qed "le_env_refl";
AddIffs [le_env_refl];
goalw thy [le_type_scheme_def,is_bound_typ_instance] "sch <= BVar n";
-by(strip_tac 1);
-by(res_inst_tac [("x","%a.t")]exI 1);
-by(Simp_tac 1);
+by (strip_tac 1);
+by (res_inst_tac [("x","%a.t")]exI 1);
+by (Simp_tac 1);
qed "bound_typ_instance_BVar";
AddIffs [bound_typ_instance_BVar];
goalw thy [le_type_scheme_def,is_bound_typ_instance] "(sch <= FVar n) = (sch = FVar n)";
-by(type_scheme.induct_tac "sch" 1);
- by(Simp_tac 1);
- by(Simp_tac 1);
- by(SELECT_GOAL(safe_tac(!claset))1);
- by(eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
- by(Asm_full_simp_tac 1);
- by(Fast_tac 1);
-by(Asm_full_simp_tac 1);
-br iffI 1;
- by(eres_inst_tac [("x","bound_typ_inst S type_scheme1 -> bound_typ_inst S type_scheme2")] allE 1);
- by(Asm_full_simp_tac 1);
- by(Fast_tac 1);
-by(Fast_tac 1);
+by (type_scheme.induct_tac "sch" 1);
+ by (Simp_tac 1);
+ by (Simp_tac 1);
+ by (SELECT_GOAL(safe_tac(!claset))1);
+ by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
+ by (Asm_full_simp_tac 1);
+ by (Fast_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac iffI 1);
+ by (eres_inst_tac [("x","bound_typ_inst S type_scheme1 -> bound_typ_inst S type_scheme2")] allE 1);
+ by (Asm_full_simp_tac 1);
+ by (Fast_tac 1);
+by (Fast_tac 1);
qed "le_FVar";
Addsimps [le_FVar];
goalw thy [le_type_scheme_def,is_bound_typ_instance] "~(FVar n <= sch1 =-> sch2)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "not_FVar_le_Fun";
AddIffs [not_FVar_le_Fun];
goalw thy [le_type_scheme_def,is_bound_typ_instance] "~(BVar n <= sch1 =-> sch2)";
-by(Simp_tac 1);
-by(res_inst_tac [("x","TVar n")] exI 1);
-by(Simp_tac 1);
-by(Fast_tac 1);
+by (Simp_tac 1);
+by (res_inst_tac [("x","TVar n")] exI 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
qed "not_BVar_le_Fun";
AddIffs [not_BVar_le_Fun];
goalw thy [le_type_scheme_def,is_bound_typ_instance]
"!!sch1. (sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'";
-by(fast_tac (!claset addss !simpset) 1);
+by (fast_tac (!claset addss !simpset) 1);
qed "Fun_le_FunD";
goal thy "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
@@ -259,33 +259,33 @@
qed_spec_mp "scheme_le_Fun";
goal thy "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch";
-by(type_scheme.induct_tac "sch" 1);
- br allI 1;
- by(type_scheme.induct_tac "sch'" 1);
- by(Simp_tac 1);
- by(Simp_tac 1);
- by(Simp_tac 1);
- br allI 1;
- by(type_scheme.induct_tac "sch'" 1);
- by(Simp_tac 1);
- by(Simp_tac 1);
- by(Simp_tac 1);
-br allI 1;
-by(type_scheme.induct_tac "sch'" 1);
- by(Simp_tac 1);
- by(Simp_tac 1);
-by(Asm_full_simp_tac 1);
-by(strip_tac 1);
-bd Fun_le_FunD 1;
-by(Fast_tac 1);
+by (type_scheme.induct_tac "sch" 1);
+ by (rtac allI 1);
+ by (type_scheme.induct_tac "sch'" 1);
+ by (Simp_tac 1);
+ by (Simp_tac 1);
+ by (Simp_tac 1);
+ by (rtac allI 1);
+ by (type_scheme.induct_tac "sch'" 1);
+ by (Simp_tac 1);
+ by (Simp_tac 1);
+ by (Simp_tac 1);
+by (rtac allI 1);
+by (type_scheme.induct_tac "sch'" 1);
+ by (Simp_tac 1);
+ by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (strip_tac 1);
+by (dtac Fun_le_FunD 1);
+by (Fast_tac 1);
qed_spec_mp "le_type_scheme_free_tv";
goal thy "!A::type_scheme list. A <= B --> free_tv B <= free_tv A";
-by(list.induct_tac "B" 1);
- by(Simp_tac 1);
-br allI 1;
-by(list.induct_tac "A" 1);
- by(simp_tac (!simpset addsimps [le_env_def]) 1);
-by(Simp_tac 1);
-by(fast_tac (!claset addDs [le_type_scheme_free_tv]) 1);
+by (list.induct_tac "B" 1);
+ by (Simp_tac 1);
+by (rtac allI 1);
+by (list.induct_tac "A" 1);
+ by (simp_tac (!simpset addsimps [le_env_def]) 1);
+by (Simp_tac 1);
+by (fast_tac (!claset addDs [le_type_scheme_free_tv]) 1);
qed_spec_mp "le_env_free_tv";
--- a/src/HOL/MiniML/MiniML.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/MiniML/MiniML.ML Wed Apr 23 11:02:19 1997 +0200
@@ -128,7 +128,7 @@
by (step_tac (!claset) 1);
by (cut_facts_tac [aux_plus] 1);
by (dtac new_tv_le 1);
-ba 1;
+by (assume_tac 1);
by (rotate_tac 1 1);
by (dtac new_tv_not_free_tv 1);
by (Fast_tac 1);
@@ -138,7 +138,7 @@
by (step_tac (!claset) 1);
by (cut_facts_tac [aux_plus] 1);
by (dtac new_tv_le 1);
-ba 1;
+by (assume_tac 1);
by (rotate_tac 1 1);
by (dtac new_tv_not_free_tv 1);
by (Fast_tac 1);
@@ -164,7 +164,7 @@
by (Asm_simp_tac 1);
by (subgoal_tac "n <= n + nat" 1);
by (dtac new_tv_le 1);
-ba 1;
+by (assume_tac 1);
by (dtac new_tv_not_free_tv 1);
by (dtac new_tv_not_free_tv 1);
by (asm_simp_tac (!simpset addsimps [diff_add_inverse ]) 1);
@@ -175,12 +175,12 @@
AddSIs has_type.intrs;
goal thy "!!e. A |- e::t ==> !B. A <= B --> B |- e::t";
-by(etac has_type.induct 1);
- by(simp_tac (!simpset addsimps [le_env_def]) 1);
- by(fast_tac (!claset addEs [bound_typ_instance_trans] addss !simpset) 1);
- by(Asm_full_simp_tac 1);
- by(Fast_tac 1);
-by(slow_tac (!claset addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1);
+by (etac has_type.induct 1);
+ by (simp_tac (!simpset addsimps [le_env_def]) 1);
+ by (fast_tac (!claset addEs [bound_typ_instance_trans] addss !simpset) 1);
+ by (Asm_full_simp_tac 1);
+ by (Fast_tac 1);
+by (slow_tac (!claset addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1);
qed_spec_mp "has_type_le_env";
(* has_type is closed w.r.t. substitution *)
@@ -220,7 +220,7 @@
val o_apply = prove_goalw HOL.thy [o_def] "(f o g) x = f (g x)"
(fn _ => [rtac refl 1]);
by (stac (S'_A_eq_S'_alpha_A) 1);
- ba 1;
+ by (assume_tac 1);
by (stac S_o_alpha_typ 1);
by (stac gen_subst_commutes 1);
by (rtac subset_antisym 1);
@@ -242,7 +242,7 @@
by (rtac has_type_le_env 1);
by (dtac spec 1);
by (dtac spec 1);
- ba 1;
+ by (assume_tac 1);
by (rtac (app_subst_Cons RS subst) 1);
by (rtac S_compatible_le_scheme_lists 1);
by (Asm_simp_tac 1);
--- a/src/HOL/MiniML/Type.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/MiniML/Type.ML Wed Apr 23 11:02:19 1997 +0200
@@ -18,15 +18,15 @@
goal thy "!t'.mk_scheme t = mk_scheme t' --> t=t'";
by (typ.induct_tac "t" 1);
- br allI 1;
+ by (rtac allI 1);
by (typ.induct_tac "t'" 1);
- by(Simp_tac 1);
- by(Asm_full_simp_tac 1);
-br allI 1;
+ by (Simp_tac 1);
+ by (Asm_full_simp_tac 1);
+by (rtac allI 1);
by (typ.induct_tac "t'" 1);
- by(Simp_tac 1);
-by(Asm_full_simp_tac 1);
-by(Fast_tac 1);
+ by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Fast_tac 1);
qed_spec_mp "mk_scheme_injective";
goal thy "!!t. free_tv (mk_scheme t) = free_tv t";
@@ -105,21 +105,21 @@
goalw thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
"new_tv n id_subst";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "new_tv_id_subst";
Addsimps[new_tv_id_subst];
goal thy "new_tv n (sch::type_scheme) --> \
\ $(%k.if k<n then S k else S' k) sch = $S sch";
by (type_scheme.induct_tac "sch" 1);
-by(ALLGOALS Asm_simp_tac);
+by (ALLGOALS Asm_simp_tac);
qed "new_if_subst_type_scheme";
Addsimps [new_if_subst_type_scheme];
goal thy "new_tv n (A::type_scheme list) --> \
\ $(%k.if k<n then S k else S' k) A = $S A";
by (list.induct_tac "A" 1);
-by(ALLGOALS Asm_simp_tac);
+by (ALLGOALS Asm_simp_tac);
qed "new_if_subst_type_scheme_list";
Addsimps [new_if_subst_type_scheme_list];
@@ -253,17 +253,17 @@
goalw thy [free_tv_subst]
"!!v. v : cod S ==> v : free_tv S";
-by( fast_tac set_cs 1);
+by ( fast_tac set_cs 1);
qed "codD";
goalw thy [free_tv_subst,dom_def]
"!! x. x ~: free_tv S ==> S x = TVar x";
-by( fast_tac set_cs 1);
+by ( fast_tac set_cs 1);
qed "not_free_impl_id";
goalw thy [new_tv_def]
"!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
-by( fast_tac HOL_cs 1 );
+by ( fast_tac HOL_cs 1 );
qed "free_tv_le_new_tv";
goalw thy [dom_def,cod_def,UNION_def,Bex_def]
@@ -278,26 +278,26 @@
goal thy
"free_tv (S (v::nat)) <= cod S Un {v}";
-by( cut_inst_tac [("P","v:dom S")] excluded_middle 1);
-by( safe_tac (HOL_cs addSIs [subsetI]) );
+by ( cut_inst_tac [("P","v:dom S")] excluded_middle 1);
+by ( safe_tac (HOL_cs addSIs [subsetI]) );
by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1);
by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1);
qed "free_tv_subst_var";
goal thy
"free_tv ($ S (t::typ)) <= cod S Un free_tv t";
-by( typ.induct_tac "t" 1);
+by ( typ.induct_tac "t" 1);
(* case TVar n *)
-by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
+by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
(* case Fun t1 t2 *)
-by( fast_tac (set_cs addss !simpset) 1);
+by ( fast_tac (set_cs addss !simpset) 1);
qed "free_tv_app_subst_te";
goal thy
"free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
-by( type_scheme.induct_tac "sch" 1);
+by ( type_scheme.induct_tac "sch" 1);
(* case FVar n *)
-by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
+by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
(* case BVar n *)
by (Simp_tac 1);
(* case Fun t1 t2 *)
@@ -306,12 +306,12 @@
goal thy
"free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
-by( list.induct_tac "A" 1);
+by ( list.induct_tac "A" 1);
(* case [] *)
by (Simp_tac 1);
(* case a#al *)
-by( cut_facts_tac [free_tv_app_subst_type_scheme] 1);
-by( fast_tac (set_cs addss !simpset) 1);
+by ( cut_facts_tac [free_tv_app_subst_type_scheme] 1);
+by ( fast_tac (set_cs addss !simpset) 1);
qed "free_tv_app_subst_scheme_list";
goalw thy [free_tv_subst,dom_def]
@@ -396,29 +396,29 @@
goalw thy [new_tv_def]
"new_tv n S = ((!m. n <= m --> (S m = TVar m)) & \
\ (! l. l < n --> new_tv n (S l) ))";
-by( safe_tac HOL_cs );
+by ( safe_tac HOL_cs );
(* ==> *)
-by( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
-by( subgoal_tac "m:cod S | S l = TVar l" 1);
-by( safe_tac HOL_cs );
-by(fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1);
-by(dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
-by(Asm_full_simp_tac 1);
-by(fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1);
+by ( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
+by ( subgoal_tac "m:cod S | S l = TVar l" 1);
+by ( safe_tac HOL_cs );
+by (fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1);
+by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1);
(* <== *)
-by( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
-by( safe_tac set_cs );
-by( cut_inst_tac [("m","m"),("n","n")] less_linear 1);
-by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
-by( cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
-by( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
+by ( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
+by ( safe_tac set_cs );
+by ( cut_inst_tac [("m","m"),("n","n")] less_linear 1);
+by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
+by ( cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
+by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
qed "new_tv_subst";
goal thy
"new_tv n = list_all (new_tv n)";
by (rtac ext 1);
-by(list.induct_tac "x" 1);
-by(ALLGOALS Asm_simp_tac);
+by (list.induct_tac "x" 1);
+by (ALLGOALS Asm_simp_tac);
qed "new_tv_list";
(* substitution affects only variables occurring freely *)
@@ -501,7 +501,7 @@
goal thy
"new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
-by( simp_tac (!simpset addsimps [new_tv_list]) 1);
+by ( simp_tac (!simpset addsimps [new_tv_list]) 1);
by (list.induct_tac "A" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "new_tv_Suc_list";
@@ -627,13 +627,13 @@
by (cut_inst_tac [("t","t")] fresh_variable_types 1);
by (cut_inst_tac [("t","t'")] fresh_variable_types 1);
by (dtac make_one_new_out_of_two 1);
-ba 1;
+by (assume_tac 1);
by (thin_tac "? n. new_tv n t'" 1);
by (cut_inst_tac [("A","A")] fresh_variable_type_scheme_lists 1);
by (cut_inst_tac [("A","A'")] fresh_variable_type_scheme_lists 1);
by (rotate_tac 1 1);
by (dtac make_one_new_out_of_two 1);
-ba 1;
+by (assume_tac 1);
by (thin_tac "? n. new_tv n A'" 1);
by (REPEAT (etac exE 1));
by (rename_tac "n2 n1" 1);
@@ -646,14 +646,14 @@
goalw thy [new_tv_def]
"!! n. [|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> \
\ new_tv n u";
-by( fast_tac (set_cs addDs [mgu_free]) 1);
+by ( fast_tac (set_cs addDs [mgu_free]) 1);
qed "mgu_new";
(* lemmata for substitutions *)
goalw Type.thy [app_subst_list] "length ($ S A) = length A";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "length_app_subst_list";
Addsimps [length_app_subst_list];
@@ -714,8 +714,8 @@
(* composition of substitutions *)
goalw Type.thy [id_subst_def,o_def] "$S o id_subst = S";
-br ext 1;
-by(Simp_tac 1);
+by (rtac ext 1);
+by (Simp_tac 1);
qed "o_id_subst";
Addsimps[o_id_subst];
@@ -747,7 +747,7 @@
goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A";
by (stac subst_id_on_type_scheme_list' 1);
-ba 1;
+by (assume_tac 1);
by (Simp_tac 1);
qed "subst_id_on_type_scheme_list";
--- a/src/HOL/MiniML/W.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/MiniML/W.ML Wed Apr 23 11:02:19 1997 +0200
@@ -70,8 +70,8 @@
goal thy "!! s. new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A";
by (dtac W_var_geD 1);
by (rtac new_scheme_list_le 1);
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
qed "new_tv_compatible_W";
goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
@@ -85,7 +85,7 @@
by (rtac new_tv_le 1);
by (mp_tac 2);
by (mp_tac 2);
-ba 2;
+by (assume_tac 2);
by (rtac add_le_mono 1);
by (Simp_tac 1);
by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
@@ -93,7 +93,7 @@
by (rtac new_tv_le 1);
by (mp_tac 2);
by (mp_tac 2);
-ba 2;
+by (assume_tac 2);
by (rtac add_le_mono 1);
by (Simp_tac 1);
by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
@@ -121,7 +121,7 @@
by (dtac sym 1);
by (dtac sym 1);
by (dtac new_tv_nth_nat_A 1);
-ba 1;
+by (assume_tac 1);
by (Asm_full_simp_tac 1);
(* case Abs e *)
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list]
@@ -146,7 +146,7 @@
by (eres_inst_tac [("x","S1")] allE 1);
by (eres_inst_tac [("x","t1")] allE 1);
by (eres_inst_tac [("x","n2")] allE 1);
-by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 1);
+by ( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 1);
by (rtac conjI 1);
by (rtac new_tv_subst_comp_2 1);
by (rtac new_tv_subst_comp_2 1);
@@ -203,9 +203,9 @@
by (rtac new_tv_subst_comp_2 1);
by (res_inst_tac [("n","n2")] new_tv_subst_le 1);
by (etac W_var_ge 1);
-ba 1;
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
by (rewtac new_tv_def);
by (Asm_simp_tac 1);
by (dtac W_var_ge 1);
@@ -356,12 +356,12 @@
by (Asm_full_simp_tac 1);
by (rtac has_type.AbsI 1);
by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1);
-bd sym 1;
+by (dtac sym 1);
by (REPEAT (etac allE 1));
by (etac impE 1);
by (mp_tac 2);
by (Asm_simp_tac 1);
-ba 1;
+by (assume_tac 1);
(* case App e1 e2 *)
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
by (strip_tac 1);
@@ -377,23 +377,23 @@
by (asm_full_simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
by (rtac (has_type_cl_sub RS spec) 1);
by (forward_tac [new_tv_W] 1);
-ba 1;
+by (assume_tac 1);
by (dtac conjunct1 1);
by (dtac conjunct1 1);
by (forward_tac [new_tv_subst_scheme_list] 1);
by (rtac new_scheme_list_le 1);
by (rtac W_var_ge 1);
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
by (etac thin_rl 1);
by (REPEAT (etac allE 1));
-bd sym 1;
-bd sym 1;
+by (dtac sym 1);
+by (dtac sym 1);
by (etac thin_rl 1);
by (etac thin_rl 1);
by (mp_tac 1);
by (mp_tac 1);
-ba 1;
+by (assume_tac 1);
(* case Let e1 e2 *)
by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
by (strip_tac 1);
@@ -421,19 +421,19 @@
by (dres_inst_tac [("x","n2")] spec 2);
by (dres_inst_tac [("x","m2")] spec 2);
by (forward_tac [new_tv_W] 2);
-ba 2;
+by (assume_tac 2);
by (dtac conjunct1 2);
by (dtac conjunct1 2);
by (forward_tac [new_tv_subst_scheme_list] 2);
by (rtac new_scheme_list_le 2);
by (rtac W_var_ge 2);
-ba 2;
-ba 2;
+by (assume_tac 2);
+by (assume_tac 2);
by (etac impE 2);
by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
by (Simp_tac 2);
by (Fast_tac 2);
-ba 2;
+by (assume_tac 2);
by (Asm_full_simp_tac 2);
by (rtac weaken_A_Int_B_eq_empty 1);
by (rtac allI 1);
@@ -443,24 +443,24 @@
by (rtac disjI2 1);
by (rtac (free_tv_gen_cons RS subst) 1);
by (rtac free_tv_W 1);
-ba 1;
+by (assume_tac 1);
by (Asm_full_simp_tac 1);
-ba 1;
+by (assume_tac 1);
by (rtac disjI1 1);
by (dtac new_tv_W 1);
-ba 1;
+by (assume_tac 1);
by (dtac conjunct2 1);
by (dtac conjunct2 1);
by (rtac new_tv_not_free_tv 1);
by (rtac new_tv_le 1);
-ba 2;
+by (assume_tac 2);
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1);
qed_spec_mp "W_correct_lemma";
goal Arith.thy "!!n::nat. ~ k+n < n";
by (nat_ind_tac "k" 1);
-by(ALLGOALS Asm_simp_tac);
-by(trans_tac 1);
+by (ALLGOALS Asm_simp_tac);
+by (trans_tac 1);
val not_add_less1 = result();
Addsimps [not_add_less1];
@@ -567,10 +567,10 @@
by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
by (case_tac "na: free_tv t - free_tv Sa" 2);
(* case na ~: free_tv t - free_tv Sa *)
-by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
+by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
by (Fast_tac 3);
(* case na : free_tv t - free_tv Sa *)
-by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
by (dtac eq_subst_scheme_list_eq_free 2);
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
@@ -579,21 +579,21 @@
by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
by (safe_tac HOL_cs );
by (dtac mgu_Some 1);
-by( fast_tac (HOL_cs addss !simpset) 1);
+by ( fast_tac (HOL_cs addss !simpset) 1);
(** LEVEL 80 *)
by ((dtac mgu_mg 1) THEN (atac 1));
by (etac exE 1);
by (res_inst_tac [("x","Rb")] exI 1);
by (rtac conjI 1);
by (dres_inst_tac [("x","ma")] fun_cong 2);
-by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
+by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
by (simp_tac (!simpset addsimps [subst_comp_scheme_list]) 1);
by (simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym]) 1);
by (res_inst_tac [("A2","($ Sa ($ S A))")]
((subst_comp_scheme_list RS sym) RSN (2,trans)) 1);
-by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
+by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
by (rtac eq_free_eq_subst_scheme_list 1);
-by( safe_tac HOL_cs );
+by ( safe_tac HOL_cs );
by (subgoal_tac "ma ~= na" 1);
by ((forward_tac [new_tv_W] 2) THEN (atac 2));
by (etac conjE 2);
@@ -632,13 +632,13 @@
by (Asm_full_simp_tac 1);
by (dtac mp 1);
by (rtac has_type_le_env 1);
-ba 1;
+by (assume_tac 1);
by (Simp_tac 1);
by (rtac gen_bound_typ_instance 1);
by (dtac mp 1);
by (forward_tac [new_tv_compatible_W] 1);
by (rtac sym 1);
-ba 1;
+by (assume_tac 1);
by (fast_tac (!claset addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1);
by (safe_tac HOL_cs);
by (Asm_full_simp_tac 1);
@@ -649,7 +649,7 @@
goal W.thy
"!!e. [] |- e :: t' ==> (? S t. (? m. W e [] n = Some(S,t,m)) & \
\ (? R. t' = $ R t))";
-by(cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
+by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
W_complete_lemma 1);
-by(ALLGOALS Asm_full_simp_tac);
+by (ALLGOALS Asm_full_simp_tac);
qed "W_complete";
--- a/src/HOL/W0/W.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/W0/W.ML Wed Apr 23 11:02:19 1997 +0200
@@ -19,7 +19,7 @@
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
setloop (split_tac [expand_bind])) 1);
by (strip_tac 1);
-bd sym 1;
+by (dtac sym 1);
by (fast_tac (HOL_cs addss !simpset) 1);
(* case App e1 e2 *)
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
--- a/src/HOL/ex/LFilter.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/ex/LFilter.ML Wed Apr 23 11:02:19 1997 +0200
@@ -19,13 +19,13 @@
goal thy "!!p. (l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
-be findRel.induct 1;
+by (etac findRel.induct 1);
by (Blast_tac 1);
by (Blast_tac 1);
qed_spec_mp "findRel_functional";
goal thy "!!p. (l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
-be findRel.induct 1;
+by (etac findRel.induct 1);
by (Blast_tac 1);
by (Blast_tac 1);
qed_spec_mp "findRel_imp_LCons";
@@ -50,7 +50,7 @@
goal thy "[| l: Domain (findRel p); \
\ !!x l'. [| (l, LCons x l') : findRel p; p x |] ==> Q \
\ |] ==> Q";
-br (major RS DomainE) 1;
+by (rtac (major RS DomainE) 1);
by (forward_tac [findRel_imp_LCons] 1);
by (REPEAT (eresolve_tac [exE,conjE] 1));
by (hyp_subst_tac 1);
@@ -60,7 +60,7 @@
val prems = goal thy
"[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
by (Step_tac 1);
-be findRel.induct 1;
+by (etac findRel.induct 1);
by (blast_tac (!claset addIs (findRel.intrs@prems)) 1);
by (blast_tac (!claset addIs findRel.intrs) 1);
qed "Domain_findRel_mono";
@@ -96,7 +96,7 @@
goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
- setloop split_tac[expand_if]) 1);
+ setloop split_tac[expand_if]) 1);
qed "find_LCons";
@@ -130,18 +130,18 @@
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
by (case_tac "LCons x l : Domain(findRel p)" 1);
by (asm_full_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
-be Domain_findRelE 1;
+by (etac Domain_findRelE 1);
by (safe_tac (!claset delrules [conjI]));
by (asm_full_simp_tac
(!simpset addsimps [findRel_imp_lfilter, findRel_imp_find,
- find_LCons_seek]) 1);
+ find_LCons_seek]) 1);
qed "lfilter_LCons_seek";
goal thy "lfilter p (LCons x l) = \
\ (if p x then LCons x (lfilter p l) else lfilter p l)";
by (asm_simp_tac (!simpset addsimps [lfilter_LCons_found, lfilter_LCons_seek]
- setloop split_tac[expand_if]) 1);
+ setloop split_tac[expand_if]) 1);
qed "lfilter_LCons";
AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
@@ -149,9 +149,9 @@
goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
-br notI 1;
-be Domain_findRelE 1;
-be rev_mp 1;
+by (rtac notI 1);
+by (etac Domain_findRelE 1);
+by (etac rev_mp 1);
by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
qed "lfilter_eq_LNil";
@@ -160,7 +160,7 @@
\ (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
by (stac (lfilter_def RS def_llist_corec) 1);
by (case_tac "l : Domain(findRel p)" 1);
-be Domain_findRelE 1;
+by (etac Domain_findRelE 1);
by (Asm_simp_tac 2);
by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
by (Blast_tac 1);
@@ -190,8 +190,8 @@
by (Step_tac 1);
(*Cases: p x is true or false*)
by (Blast_tac 1);
-br (lfilter_cases RS disjE) 1;
-be ssubst 1;
+by (rtac (lfilter_cases RS disjE) 1);
+by (etac ssubst 1);
by (Auto_tac());
qed "lfilter_idem";
@@ -202,7 +202,7 @@
goal thy "!!p. (l,l') : findRel q \
\ ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
-be findRel.induct 1;
+by (etac findRel.induct 1);
by (blast_tac (!claset addIs findRel.intrs) 1);
by (blast_tac (!claset addIs findRel.intrs) 1);
qed_spec_mp "findRel_conj_lemma";
@@ -212,7 +212,7 @@
goal thy "!!p. (l,l'') : findRel (%x. p x & q x) \
\ ==> (l, LCons x l') : findRel q --> ~ p x \
\ --> l' : Domain (findRel (%x. p x & q x))";
-be findRel.induct 1;
+by (etac findRel.induct 1);
by (Auto_tac());
qed_spec_mp "findRel_not_conj_Domain";
@@ -220,7 +220,7 @@
goal thy "!!p. (l,lxx) : findRel q ==> \
\ lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
\ --> (l,lz) : findRel (%x. p x & q x)";
-be findRel.induct 1;
+by (etac findRel.induct 1);
by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
qed_spec_mp "findRel_conj2";
@@ -228,14 +228,14 @@
goal thy "!!p. (lx,ly) : findRel p \
\ ==> ALL l. lx = lfilter q l \
\ --> l : Domain (findRel(%x. p x & q x))";
-be findRel.induct 1;
+by (etac findRel.induct 1);
by (blast_tac (!claset addSDs [sym RS lfilter_eq_LCons]
- addIs [findRel_conj]) 1);
+ addIs [findRel_conj]) 1);
by (Auto_tac());
-bd (sym RS lfilter_eq_LCons) 1;
+by (dtac (sym RS lfilter_eq_LCons) 1);
by (Auto_tac());
-bd spec 1;
-bd (refl RS rev_mp) 1;
+by (dtac spec 1);
+by (dtac (refl RS rev_mp) 1);
by (blast_tac (!claset addIs [findRel_conj2]) 1);
qed_spec_mp "findRel_lfilter_Domain_conj";
@@ -243,7 +243,7 @@
goal thy "!!p. (l,l'') : findRel(%x. p x & q x) \
\ ==> l'' = LCons y l' --> \
\ (lfilter q l, LCons y (lfilter q l')) : findRel p";
-be findRel.induct 1;
+by (etac findRel.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
qed_spec_mp "findRel_conj_lfilter";
@@ -263,7 +263,7 @@
(*case q x*)
by (case_tac "p x" 1);
by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter,
- findRel_conj RS findRel_imp_lfilter]) 1);
+ findRel_conj RS findRel_imp_lfilter]) 1);
by (Blast_tac 1);
(*case q x and ~(p x) *)
by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
@@ -276,7 +276,7 @@
(* ...and therefore too, no p in lfilter q l'. Both results are Lnil*)
by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
(*subcase: there is a p&q in l' and therefore also one in l*)
-be Domain_findRelE 1;
+by (etac Domain_findRelE 1);
by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
by (blast_tac (!claset addIs [findRel_conj2]) 2);
by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
@@ -298,7 +298,7 @@
***)
goal thy "!!p. (l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
-be findRel.induct 1;
+by (etac findRel.induct 1);
by (ALLGOALS Asm_full_simp_tac);
qed "findRel_lmap_Domain";
@@ -315,7 +315,7 @@
\ ALL l. lmap f l = lx --> ly = LCons x l' --> \
\ (EX y l''. x = f y & l' = lmap f l'' & \
\ (l, LCons y l'') : findRel(%x. p(f x)))";
-be findRel.induct 1;
+by (etac findRel.induct 1);
by (ALLGOALS Asm_simp_tac);
by (safe_tac (!claset addSDs [lmap_eq_LCons]));
by (blast_tac (!claset addIs findRel.intrs) 1);
@@ -333,7 +333,7 @@
by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
by (blast_tac (!claset addIs [findRel_lmap_Domain]) 3);
by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
-be Domain_findRelE 1;
+by (etac Domain_findRelE 1);
by (forward_tac [lmap_LCons_findRel] 1);
by (Step_tac 1);
by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
--- a/src/HOL/ex/LList.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOL/ex/LList.ML Wed Apr 23 11:02:19 1997 +0200
@@ -649,7 +649,7 @@
goalw thy [llistD_Fun_def, prod_fun_def]
"!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
by (Auto_tac());
-br image_eqI 1;
+by (rtac image_eqI 1);
by (fast_tac (!claset addss (!simpset)) 1);
by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
qed "llistD_Fun_mono";
--- a/src/HOLCF/Discrete0.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOLCF/Discrete0.ML Wed Apr 23 11:02:19 1997 +0200
@@ -7,16 +7,16 @@
*)
goalw thy [less_discr_def] "less (x::('a::term)discr) x";
-br refl 1;
+by (rtac refl 1);
qed "less_discr_refl";
goalw thy [less_discr_def]
"!!x. [| less (x::('a::term)discr) y; less y z |] ==> less x z";
-be trans 1;
-ba 1;
+by (etac trans 1);
+by (assume_tac 1);
qed "less_discr_trans";
goalw thy [less_discr_def]
"!!x. [| less (x::('a::term)discr) y; less y x |] ==> x=y";
-ba 1;
+by (assume_tac 1);
qed "less_discr_antisym";
--- a/src/HOLCF/Discrete1.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOLCF/Discrete1.ML Wed Apr 23 11:02:19 1997 +0200
@@ -7,26 +7,26 @@
*)
goalw thy [po_def,less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
-br refl 1;
+by (rtac refl 1);
qed "discr_less_eq";
AddIffs [discr_less_eq];
goalw thy [is_chain]
"!!S::nat=>('a::term)discr. is_chain S ==> S i = S 0";
-by(nat_ind_tac "i" 1);
- br refl 1;
-be subst 1;
-br sym 1;
-by(Fast_tac 1);
+by (nat_ind_tac "i" 1);
+ by (rtac refl 1);
+by (etac subst 1);
+by (rtac sym 1);
+by (Fast_tac 1);
qed "discr_chain0";
goal thy
"!!S::nat=>('a::term)discr. is_chain(S) ==> range(S) = {S 0}";
-by(fast_tac (!claset addEs [discr_chain0]) 1);
+by (fast_tac (!claset addEs [discr_chain0]) 1);
qed "discr_chain_range0";
Addsimps [discr_chain_range0];
goalw thy [is_lub,is_ub]
"!!S. is_chain S ==> ? x::('a::term)discr. range(S) <<| x";
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed "discr_cpo";
--- a/src/HOLCF/Porder.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOLCF/Porder.ML Wed Apr 23 11:02:19 1997 +0200
@@ -137,8 +137,8 @@
goal thy "lub{x} = x";
-br thelubI 1;
-by(simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
+by (rtac thelubI 1);
+by (simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
qed "lub_singleton";
Addsimps [lub_singleton];
--- a/src/HOLCF/ex/Focus_ex.ML Wed Apr 23 11:00:48 1997 +0200
+++ b/src/HOLCF/ex/Focus_ex.ML Wed Apr 23 11:02:19 1997 +0200
@@ -75,7 +75,7 @@
by (strip_tac 1);
by (rtac fix_least 1);
by (Simp_tac 1);
-by(etac exE 1);
+by (etac exE 1);
by (dtac sym 1);
back();
by (asm_simp_tac HOLCF_ss 1);
@@ -84,7 +84,7 @@
(* direction is_g(g) --> def_g(g) *)
val prems = goal Focus_ex.thy "is_g(g) --> def_g(g)";
by (simp_tac (HOL_ss delsimps (ex_simps @ all_simps)
- addsimps [lemma1,lemma2,def_g]) 1);
+ addsimps [lemma1,lemma2,def_g]) 1);
by (rtac impI 1);
by (etac exE 1);
by (res_inst_tac [("x","f")] exI 1);