--- a/src/HOL/IOA/meta_theory/IOA.ML Mon Oct 07 10:26:00 1996 +0200
+++ b/src/HOL/IOA/meta_theory/IOA.ML Mon Oct 07 10:28:44 1996 +0200
@@ -54,23 +54,22 @@
goalw IOA.thy (reachable_def::exec_rws)
"!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
- by(Asm_full_simp_tac 1);
- by(safe_tac (!claset));
- by(res_inst_tac [("x","(%i.if i<n then fst ex i \
+ by (Asm_full_simp_tac 1);
+ by (safe_tac (!claset));
+ by (res_inst_tac [("x","(%i.if i<n then fst ex i \
\ else (if i=n then Some a else None), \
\ %i.if i<Suc n then snd ex i else t)")] bexI 1);
- by(res_inst_tac [("x","Suc(n)")] exI 1);
- by(Simp_tac 1);
- by(Asm_simp_tac 1);
- by(REPEAT(rtac allI 1));
- by(res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1);
- be disjE 1;
- by(asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
- be disjE 1;
- by(Asm_simp_tac 1);
- by(Fast_tac 1);
- by(forward_tac [less_not_sym] 1);
- by(asm_simp_tac (!simpset addsimps [less_not_refl2,less_Suc_eq]) 1);
+ by (res_inst_tac [("x","Suc(n)")] exI 1);
+ by (Simp_tac 1);
+ by (Asm_simp_tac 1);
+ by (REPEAT(rtac allI 1));
+ by (res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1);
+ by (etac disjE 1);
+ by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
+ by (etac disjE 1);
+ by (Asm_simp_tac 1);
+ by (forward_tac [less_not_sym] 1);
+ by (asm_simp_tac (!simpset addsimps [less_not_refl2,less_Suc_eq]) 1);
qed "reachable_n";
val [p1,p2] = goalw IOA.thy [invariant_def]
@@ -100,19 +99,19 @@
val [p1,p2] = goalw IOA.thy [invariant_def]
"[| invariant A P; reachable A s |] ==> P(s)";
- br(p2 RS (p1 RS spec RS mp))1;
+ by (rtac (p2 RS (p1 RS spec RS mp)) 1);
qed "invariantE";
goal IOA.thy
"actions(asig_comp a b) = actions(a) Un actions(b)";
- by(simp_tac (!simpset addsimps
+ by (simp_tac (!simpset addsimps
([actions_def,asig_comp_def]@asig_projections)) 1);
- by(Fast_tac 1);
+ by (Fast_tac 1);
qed "actions_asig_comp";
goal IOA.thy
"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
- by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+ by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
qed "starts_of_par";
(* Every state in an execution is reachable *)
@@ -136,7 +135,7 @@
\ (if a:actions(asig_of(D)) then \
\ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \
\ else snd(snd(snd(t)))=snd(snd(snd(s)))))";
- by(simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
+ by (simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
ioa_projections)
setloop (split_tac [expand_if])) 1);
qed "trans_of_par4";
@@ -144,12 +143,12 @@
goal IOA.thy "starts_of(restrict ioa acts) = starts_of(ioa) & \
\ trans_of(restrict ioa acts) = trans_of(ioa) & \
\ reachable (restrict ioa acts) s = reachable ioa s";
-by(simp_tac (!simpset addsimps ([is_execution_fragment_def,executions_def,
+by (simp_tac (!simpset addsimps ([is_execution_fragment_def,executions_def,
reachable_def,restrict_def]@ioa_projections)) 1);
qed "cancel_restrict";
goal IOA.thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
- by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+ by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
qed "asig_of_par";
--- a/src/HOL/Lex/Auto.ML Mon Oct 07 10:26:00 1996 +0200
+++ b/src/HOL/Lex/Auto.ML Mon Oct 07 10:28:44 1996 +0200
@@ -34,6 +34,5 @@
by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
by(res_inst_tac [("x","x#us")] exI 1);
by(Asm_simp_tac 1);
-by (Fast_tac 1);
qed"acc_prefix_Cons";
Addsimps [acc_prefix_Cons];
--- a/src/HOL/Lex/AutoChopper.ML Mon Oct 07 10:26:00 1996 +0200
+++ b/src/HOL/Lex/AutoChopper.ML Mon Oct 07 10:28:44 1996 +0200
@@ -31,10 +31,10 @@
by (strip_tac 1);
by (rtac conjI 1);
by (Fast_tac 1);
-by(simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1);
+by (simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1);
by (strip_tac 1);
-by(REPEAT(eresolve_tac [conjE,exE] 1));
-by(hyp_subst_tac 1);
+by (REPEAT(eresolve_tac [conjE,exE] 1));
+by (hyp_subst_tac 1);
by (Simp_tac 1);
by (case_tac "zsa = []" 1);
by (Asm_simp_tac 1);
@@ -55,14 +55,14 @@
by (list.induct_tac "xs" 1);
by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
-by(rename_tac "vss lrst" 1);
+by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by (rename_tac "vss lrst" 1);
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (res_inst_tac[("xs","vss")] list_eq_cases 1);
- by(hyp_subst_tac 1);
- by(Simp_tac 1);
+ by (hyp_subst_tac 1);
+ by (Simp_tac 1);
by (fast_tac (!claset addSDs [no_acc]) 1);
-by(hyp_subst_tac 1);
+by (hyp_subst_tac 1);
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
val step2_a = (result() repeat_RS spec) RS mp;
@@ -78,12 +78,12 @@
by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
by (Fast_tac 1);
by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
-by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
-by(rename_tac "vss lrst" 1);
-by(Asm_simp_tac 1);
+by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by (rename_tac "vss lrst" 1);
+by (Asm_simp_tac 1);
by (strip_tac 1);
by (case_tac "acc_prefix A (next A st a) list" 1);
- by(Asm_simp_tac 1);
+ by (Asm_simp_tac 1);
by (subgoal_tac "r @ [a] ~= []" 1);
by (Fast_tac 1);
by (Simp_tac 1);
@@ -103,9 +103,9 @@
by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
by (strip_tac 1);
by (rtac conjI 1);
- by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
- by(rename_tac "vss lrst" 1);
- by(Asm_simp_tac 1);
+ by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+ by (rename_tac "vss lrst" 1);
+ by (Asm_simp_tac 1);
by (case_tac "acc_prefix A (next A st a) list" 1);
by (strip_tac 1);
by (res_inst_tac [("f","%k.a#k")] ex_special 1);
@@ -117,7 +117,7 @@
by (res_inst_tac [("x","[a]")] exI 1);
by (Asm_simp_tac 1);
by (subgoal_tac "r @ [a] ~= []" 1);
- br sym 1;
+ by (rtac sym 1);
by (Fast_tac 1);
by (Simp_tac 1);
by (strip_tac 1);
@@ -140,9 +140,9 @@
by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
by (Fast_tac 1);
by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
-by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
-by(rename_tac "vss lrst" 1);
-by(Asm_simp_tac 1);
+by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by (rename_tac "vss lrst" 1);
+by (Asm_simp_tac 1);
by (strip_tac 1);
by (case_tac "acc_prefix A (next A st a) list" 1);
by (Asm_simp_tac 1);
@@ -152,8 +152,8 @@
by (Fast_tac 2);
by (Simp_tac 2);
by (subgoal_tac "flat(yss) @ zs = list" 1);
- by(hyp_subst_tac 1);
- by(atac 1);
+ by (hyp_subst_tac 1);
+ by (atac 1);
by (case_tac "yss = []" 1);
by (Asm_simp_tac 1);
by (hyp_subst_tac 1);
@@ -163,7 +163,7 @@
by (hyp_subst_tac 1);
by (Simp_tac 1);
by (rtac trans 1);
- be step2_a 1;
+ by (etac step2_a 1);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
val step2_d = (result() repeat_RS spec) RS mp;
@@ -181,7 +181,7 @@
by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
by (strip_tac 1);
by (case_tac "acc_prefix A (next A st a) list" 1);
- br conjI 1;
+ by (rtac conjI 1);
by (strip_tac 1);
by (res_inst_tac [("f","%k.a#k")] ex_special 1);
by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
@@ -190,7 +190,7 @@
by (asm_simp_tac HOL_ss 1);
by (res_inst_tac [("x","x")] exI 1);
by (Asm_simp_tac 1);
- br list_cases 1;
+ by (rtac list_cases 1);
by (Simp_tac 1);
by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
by (strip_tac 1);
@@ -201,7 +201,7 @@
by (asm_simp_tac HOL_ss 1);
by (res_inst_tac [("x","x")] exI 1);
by (Asm_simp_tac 1);
- br list_cases 1;
+ by (rtac list_cases 1);
by (Simp_tac 1);
by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
by (Asm_simp_tac 1);
@@ -223,22 +223,20 @@
Chopper.is_longest_prefix_chopper_def]
"is_auto_chopper(auto_chopper)";
by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
- br mp 1;
- be step2_b 2;
+ by (rtac mp 1);
+ by (etac step2_b 2);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (rtac conjI 1);
- br mp 1;
- be step2_c 2;
+ by (rtac mp 1);
+ by (etac step2_c 2);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
- by (Fast_tac 1);
by (rtac conjI 1);
by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
by (rtac conjI 1);
- br mp 1;
- be step2_d 2;
+ by (rtac mp 1);
+ by (etac step2_d 2);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (rtac mp 1);
- be step2_e 2;
+ by (etac step2_e 2);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (Fast_tac 1);
qed"auto_chopper_is_auto_chopper";
--- a/src/HOL/Option.ML Mon Oct 07 10:26:00 1996 +0200
+++ b/src/HOL/Option.ML Mon Oct 07 10:28:44 1996 +0200
@@ -27,5 +27,4 @@
by (option.induct_tac "opt" 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
-by (Fast_tac 1);
qed"expand_option_case";
--- a/src/HOL/RelPow.ML Mon Oct 07 10:26:00 1996 +0200
+++ b/src/HOL/RelPow.ML Mon Oct 07 10:28:44 1996 +0200
@@ -26,7 +26,6 @@
goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)";
by (nat_ind_tac "n" 1);
by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by (Fast_tac 1);
by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
by (Fast_tac 1);
qed_spec_mp "rel_pow_Suc_I2";