isatool expandshort;

--- a/src/HOLCF/Cfun2.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/HOLCF/Cfun2.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -94,9 +94,9 @@
 (* ?x2 << ?x1 ==> ?fo5$?x2 << ?fo5$?x1                                      *)
 
 Goal "chain Y ==> chain (%i. f\\<cdot>(Y i))";
-br chainI 1;
-br monofun_cfun_arg 1;
-be chainE 1;
+by (rtac chainI 1);
+by (rtac monofun_cfun_arg 1);
+by (etac chainE 1);
 qed "chain_monofun";
 
 

--- a/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -86,7 +86,7 @@
  (K [
 	rtac (BufAC_Cmt_unfold RS iffD2) 1,
 	strip_tac 1,
-	forward_tac [Buf_f_d_req] 1,
+	ftac Buf_f_d_req 1,
 	auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
 
 (*adm_BufAC_Asm*)
@@ -118,7 +118,7 @@
 by (strip_tac 1);
 by (stac BufAC_Cmt_F_def3 1);
 by (dres_inst_tac [("P","%x. x")] (BufAC_Cmt_F_def3 RS subst) 1);
-by (Safe_tac);
+by Safe_tac;
 by (   etac Buf_f_empty 1);
 by (  etac Buf_f_d 1);
 by ( dtac Buf_f_d_req 1);
@@ -215,8 +215,8 @@
 (**** new approach for admissibility, reduces itself to absurdity *************)
 
 Goal "adm (\\<lambda>x. x\\<in>BufAC_Asm)";
-by(rtac def_gfp_admI 1);
-by(rtac BufAC_Asm_def 1);
+by (rtac def_gfp_admI 1);
+by (rtac BufAC_Asm_def 1);
 b y Safe_tac;
 b y rewtac BufAC_Asm_F_def;
 b y Safe_tac;
@@ -238,7 +238,7 @@
 b y Clarsimp_tac 1;
 b y simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1;
 b y res_inst_tac [("x","Xa")] exI 1;
-br allI 1;
+by (rtac allI 1);
 b y rotate_tac ~1 1;
 b y eres_inst_tac [("x","i")] allE 1;
 b y Clarsimp_tac 1;
@@ -271,8 +271,8 @@
 qed "adm_non_BufAC_Asm";
 
 Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
-by(rtac triv_admI 1);
-by(Clarify_tac 1);
-by(eatac Buf_Eq_imp_AC_lemma 1 1); 
+by (rtac triv_admI 1);
+by (Clarify_tac 1);
+by (eatac Buf_Eq_imp_AC_lemma 1 1); 
       (* this is what we originally aimed to show, using admissibilty :-( *)
 qed "adm_BufAC";

--- a/src/HOLCF/Pcpo.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/HOLCF/Pcpo.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -52,18 +52,18 @@
 
 Goal "chain (Y::nat=>'a::cpo) ==> lub(range (%i. Y(i + j))) = lub(range Y)";
 by (rtac antisym_less 1);
-br lub_range_mono 1;
+by (rtac lub_range_mono 1);
 by    (Fast_tac 1);
 by   (atac 1);
-be  chain_shift 1;
-br is_lub_thelub 1;
-ba  1;
-br ub_rangeI 1;
-br trans_less 1;
-br  is_ub_thelub 2;
-be  chain_shift 2;
-be chain_mono3 1;
-br le_add1 1;
+by (etac chain_shift 1);
+by (rtac is_lub_thelub 1);
+by (assume_tac 1);
+by (rtac ub_rangeI 1);
+by (rtac trans_less 1);
+by (rtac is_ub_thelub 2);
+by (etac chain_shift 2);
+by (etac chain_mono3 1);
+by (rtac le_add1 1);
 qed "lub_range_shift";
 
 Goal "chain Y ==> max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))";

--- a/src/HOLCF/Porder.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/HOLCF/Porder.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -38,7 +38,7 @@
 (* ------------------------------------------------------------------------ *)
 
 Goalw [tord_def] "chain(F) ==> tord(range(F))";
-by (Safe_tac);
+by Safe_tac;
 by (rtac nat_less_cases 1);
 by (ALLGOALS (fast_tac (claset() addIs [chain_mono])));
 qed "chain_tord";
@@ -92,9 +92,9 @@
 qed "chainI";
 
 Goal "chain Y ==> chain (%i. Y (i + j))";
-br chainI 1;
+by (rtac chainI 1);
 by (Clarsimp_tac 1);
-be chainE 1;
+by (etac chainE 1);
 qed "chain_shift";
 
 (* ------------------------------------------------------------------------ *)

--- a/src/HOLCF/ex/Stream.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/HOLCF/ex/Stream.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -28,7 +28,7 @@
 qed "scons_eq_UU";
 
 Goal "[| a && x = UU; a ~= UU |] ==> R";
-by (dresolve_tac [stream_con_rew2] 1);
+by (dtac stream_con_rew2 1);
 by (contr_tac 1);
 qed "scons_not_empty";
 
@@ -534,7 +534,7 @@
 \!s. #(s::'a::flat stream) = #t &  s << t --> s = t";
 by (etac stream_finite_ind 1);
 by  (fast_tac (claset() addDs [eq_UU_iff RS iffD2]) 1);
-by (Safe_tac);
+by Safe_tac;
 by (stream_case_tac "sa" 1);
 by  (dtac sym 1);
 by  (Asm_full_simp_tac 1);

--- a/src/ZF/Induct/FoldSet.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/Induct/FoldSet.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -37,7 +37,7 @@
 
 Goal "[| <C-{x},y> : fold_set(A, B, f,e);  x:C; x:A |] \
 \     ==> <C, f(x,y)> : fold_set(A, B, f, e)";
-by (forward_tac [fold_set_rhs] 1);
+by (ftac fold_set_rhs 1);
 by (etac (cons_Diff RS subst) 1 THEN resolve_tac fold_set.intrs 1);
 by (auto_tac (claset() addIs [f_type], simpset()));
 qed "Diff1_fold_set";
@@ -45,7 +45,7 @@
 Goal "[| C:Fin(A); e:B |] ==> EX x. <C, x> : fold_set(A, B, f,e)";
 by (etac Fin_induct 1);
 by (ALLGOALS(Clarify_tac));
-by (forward_tac [fold_set_rhs] 2);
+by (ftac fold_set_rhs 2);
 by (cut_inst_tac [("x", "x"), ("y", "xa")] f_type 2);
 by (REPEAT(blast_tac (claset() addIs fold_set.intrs) 1));
 qed_spec_mp "Fin_imp_fold_set";
@@ -104,7 +104,7 @@
 Goal "[| <C, x> : fold_set(A, B, f, e); \
 \        <C, y> : fold_set(A, B, f, e); e:B |] ==> y=x";
 by (forward_tac [fold_set_lhs RS Fin_into_Finite] 1);
-by (rewrite_goals_tac [Finite_def]);
+by (rewtac Finite_def);
 by (Clarify_tac 1);
 by (res_inst_tac [("n", "succ(n)")] lemma 1);
 by (auto_tac (claset() addIs 
@@ -171,7 +171,7 @@
 by Auto_tac;
 by (resolve_tac [fold_set_mono RS subsetD] 1);
 by (Blast_tac 2);
-by (dresolve_tac [fold_set_mono2] 3);
+by (dtac fold_set_mono2 3);
 by (auto_tac (claset() addIs [Fin_imp_fold_set],
               simpset() addsimps [symmetric fold_def, fold_equality]));
 qed "fold_cons";
@@ -328,10 +328,10 @@
 by (Blast_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [major,subset_cons_iff]@prems) 1);
 by Safe_tac;
-by (forward_tac [subset_Finite] 1);
+by (ftac subset_Finite 1);
 by (assume_tac 1);
 by (Blast_tac 1);
-by (forward_tac [subset_Finite] 1);
+by (ftac subset_Finite 1);
 by (assume_tac 1);
 by (subgoal_tac "C = cons(x, C - {x})" 1);
 by (Blast_tac 2);
@@ -377,7 +377,7 @@
 by (case_tac "Finite(A)" 1);
 by (blast_tac (claset() 
      addIs [setsum_succD_lemma RS bspec RS mp]) 1);
-by (rewrite_goals_tac [setsum_def]);
+by (rewtac setsum_def);
 by (auto_tac (claset(), 
        simpset() delsimps [int_of_0, int_of_succ] 
                  addsimps [int_succ_int_1 RS sym, int_of_0 RS sym]));

--- a/src/ZF/Induct/Multiset.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/Induct/Multiset.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -106,7 +106,7 @@
 Goalw [mdiff_def, multiset_def]
  "[| multiset(M); mset_of(M)<=A |] ==> mset_of(M -# N) <= A";
 by (auto_tac (claset(), simpset() addsimps [normalize_def]));
-by (rewrite_goals_tac [mset_of_def]);
+by (rewtac mset_of_def);
 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [multiset_fun_iff])));
 by (ALLGOALS(Clarify_tac));
 by (ALLGOALS(rotate_simp_tac "M:?u"));
@@ -242,7 +242,7 @@
 by (rewrite_goals_tac [munion_def, mdiff_def, 
                        msingle_def, normalize_def, mset_of_def]);
 by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
-by (resolve_tac [fun_extension] 1);
+by (rtac fun_extension 1);
 by Auto_tac;
 by (res_inst_tac [("P", "%x. ?u : Pi(x, ?v)")] subst 1);
 by (rtac restrict_type 2);
@@ -546,7 +546,7 @@
 \ (setsum(%x. $# mcount(M, x), {x:mset_of(M). 0 < M`x}) = $# n) --> P(M))";
 by (rtac (major RS nat_induct) 1);
 by (ALLGOALS(Clarify_tac));
-by (forward_tac [msize_eq_0_iff] 1);
+by (ftac msize_eq_0_iff 1);
 by (auto_tac (claset(), 
               simpset() addsimps [mset_of_def, multiset_def,  
                                   multiset_fun_iff, msize_def]@prems));
@@ -632,7 +632,7 @@
  \   ==> P(M)";
 by (subgoal_tac "EX n:nat. setsum(\\<lambda>x. $# mcount(M, x), \
               \ {x : mset_of(M) . 0 < M ` x}) = $# n" 1);
-by (resolve_tac [not_zneg_int_of] 2);
+by (rtac not_zneg_int_of 2);
 by (ALLGOALS(asm_simp_tac (simpset() 
         addsimps [znegative_iff_zless_0, not_zless_iff_zle])));
 by (rtac g_zpos_imp_setsum_zpos 2);
@@ -649,7 +649,7 @@
 Goalw [multiset_def, msingle_def] 
  "[| multiset(M); a ~:mset_of(M) |] ==> M +# {#a#} = cons(<a, 1>, M)";
 by (auto_tac (claset(), simpset() addsimps [munion_def]));
-by (rewrite_goals_tac [mset_of_def]);
+by (rewtac mset_of_def);
 by (rotate_simp_tac "M:?u" 1);
 by (rtac fun_extension 1 THEN rtac lam_type 1);
 by (ALLGOALS(Asm_full_simp_tac));
@@ -666,7 +666,7 @@
 "[| multiset(M); a:mset_of(M) |] ==> M +# {#a#} = M(a:=M`a #+ 1)";
 by (auto_tac (claset(),  simpset() 
      addsimps [munion_def, multiset_fun_iff, msingle_def]));
-by (rewrite_goals_tac [mset_of_def]);
+by (rewtac mset_of_def);
 by (rotate_simp_tac "M:?u" 1);
 by (subgoal_tac "A Un {a} = A" 1);
 by (rtac fun_extension 1);
@@ -776,9 +776,9 @@
 
 Goalw [multiset_on_def, multiset_def, mset_of_def]
  "M:A-||>nat-{0} ==> multiset[A](M)";
-by (forward_tac [FiniteFun_is_fun] 1);
+by (ftac FiniteFun_is_fun 1);
 by (dtac FiniteFun_domain_Fin 1);
-by (forward_tac [FinD] 1);
+by (ftac FinD 1);
 by (Clarify_tac 1);
 by (res_inst_tac [("x", "domain(M)")] exI 1);
 by (blast_tac (claset() addIs [Fin_into_Finite]) 1);
@@ -861,19 +861,19 @@
 Goal "[| <N, M0 +# {#a#}>:multirel1(A, r); multiset[A](M0) |] ==> \
 \ (EX M. <M, M0>:multirel1(A, r) & N = M +# {#a#}) | \
 \ (EX K. multiset[A](K) & (ALL b:mset_of(K). <b, a>:r) & N = M0 +# K)";
-by (forward_tac [multirel1D] 1);
+by (ftac multirel1D 1);
 by (asm_full_simp_tac (simpset() addsimps [multirel1_iff]) 1);
 by (auto_tac (claset(), simpset() addsimps [munion_eq_conv_exist]));
 by (ALLGOALS(res_inst_tac [("x", "Ka +# K")] exI));
 by Auto_tac;
-by (rewrite_goals_tac [multiset_on_def]);
+by (rewtac multiset_on_def);
 by (asm_simp_tac (simpset() addsimps [munion_left_cancel, munion_assoc]) 1);
 by (auto_tac (claset(), simpset() addsimps [munion_commute]));
 qed "less_munion";
 
 Goal "[| multiset[A](M); a:A |] ==> <M, M +# {#a#}>: multirel1(A, r)";
 by (auto_tac (claset(), simpset() addsimps [multirel1_iff]));
-by (rewrite_goals_tac [multiset_on_def]);
+by (rewtac multiset_on_def);
 by (res_inst_tac [("x", "a")] exI 1);
 by (Clarify_tac 1);
 by (res_inst_tac [("x", "M")] exI 1);
@@ -1112,7 +1112,7 @@
 by Auto_tac;
 by (res_inst_tac [("x", "a")] exI 1);
 by (res_inst_tac [("x", "M -# {#a#}")] exI 1);
-by (forward_tac [multiset_on_imp_multiset] 1);
+by (ftac multiset_on_imp_multiset 1);
 by (Asm_simp_tac 1);
 by (auto_tac (claset(), simpset() addsimps [multiset_on_def]));
 qed "msize_eq_succ_imp_eq_union";
@@ -1133,7 +1133,7 @@
 by (subgoal_tac "msize(J)=$# succ(x)" 1);
 by (Asm_simp_tac 2);
 by (forw_inst_tac [("A", "A")]  msize_eq_succ_imp_eq_union 1);
-by (rewrite_goals_tac [multiset_on_def]);
+by (rewtac multiset_on_def);
 by (Clarify_tac 3 THEN rotate_tac ~1 3);
 by (ALLGOALS(Asm_full_simp_tac));
 by (rename_tac  "J'" 1);
@@ -1245,7 +1245,7 @@
 
 Goal
 "[|<M,N>:multirel1(A, r); multiset[A](K)|] ==> <K +# M, K +# N>: multirel1(A, r)";
-by (forward_tac [multirel1D] 1);
+by (ftac multirel1D 1);
 by (auto_tac (claset(), simpset() addsimps [multirel1_iff, multiset_on_def]));
 by (res_inst_tac [("x", "a")] exI 1); 
 by (Asm_simp_tac 1);
@@ -1258,7 +1258,7 @@
 
 Goal
  "[| <M, N>:multirel(A, r); multiset[A](K) |]==><K +# M, K +# N>:multirel(A, r)";
-by (forward_tac [multirelD] 1);
+by (ftac multirelD 1);
 by (full_simp_tac (simpset() addsimps [multirel_def]) 1);
 by (Clarify_tac 1);
 by (dres_inst_tac [("psi", "<M,N>:multirel1(A, r)^+")] asm_rl 1);
@@ -1278,11 +1278,11 @@
 
 Goal 
 "[|<M, N>:multirel(A, r); multiset[A](K)|] ==> <M +# K, N +# K>:multirel(A, r)";
-by (forward_tac [multirelD] 1);
+by (ftac multirelD 1);
 by (res_inst_tac [("P", "%x. <x,?u>:multirel(A, r)")] (munion_commute RS subst) 1);
 by (stac (munion_commute RS sym) 3);
 by (rtac munion_multirel_mono2 5); 
-by (rewrite_goals_tac [multiset_on_def]);
+by (rewtac multiset_on_def);
 by Auto_tac;
 qed "munion_multirel_mono1";
 
@@ -1468,7 +1468,7 @@
   "[| M <#= K;  N <#= L |] ==> M +# N <#= K +# L";
 by (forw_inst_tac [("M", "M")] mle_imp_omultiset 1);
 by (forw_inst_tac [("M", "N")] mle_imp_omultiset 1);
-by (rewrite_goals_tac [mle_def]);
+by (rewtac mle_def);
 by (ALLGOALS(Asm_full_simp_tac));
 by (REPEAT(etac disjE 1));
 by (etac disjE 3);

--- a/src/ZF/UNITY/Comp.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/UNITY/Comp.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -96,7 +96,7 @@
 qed "Join_component_iff";
 
 Goal "[| F component G; G:A co B; F:program |] ==> F : A co B";
-by (forward_tac [constrainsD2] 1);
+by (ftac constrainsD2 1);
 by (rotate_tac ~1 1);
 by (auto_tac (claset(), 
               simpset() addsimps [constrains_def, component_eq_subset]));

--- a/src/ZF/UNITY/Constrains.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/UNITY/Constrains.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -18,7 +18,7 @@
 qed "reachable_type";
 
 Goalw [st_set_def] "st_set(reachable(F))";
-by (resolve_tac [reachable_type] 1);
+by (rtac reachable_type 1);
 qed "st_set_reachable";
 AddIffs [st_set_reachable];
 
@@ -168,7 +168,7 @@
 by (asm_simp_tac (simpset() delsimps INT_simps
 	  	 	    addsimps [Constrains_def]@INT_extend_simps) 1);
 by (rtac constrains_INT 1);
-by (dresolve_tac [major] 1);
+by (dtac major 1);
 by (auto_tac (claset(), simpset() addsimps [Constrains_def])); 
 qed "Constrains_INT";
 
@@ -325,7 +325,7 @@
 
 (*the RHS is the traditional definition of the "always" operator*)
 Goal "Always(A) = {F:program. reachable(F) <= A}";
-br equalityI 1;
+by (rtac equalityI 1);
 by (ALLGOALS(Clarify_tac));
 by (auto_tac (claset() addDs [invariant_includes_reachable],
               simpset() addsimps [subset_Int_iff, invariant_reachable,
@@ -337,7 +337,7 @@
 qed "Always_type";
 
 Goal "Always(state) = program";
-br equalityI 1;
+by (rtac equalityI 1);
 by (auto_tac (claset() addDs [Always_type RS subsetD, 
                               reachable_type RS subsetD], 
               simpset() addsimps [Always_eq_includes_reachable]));

--- a/src/ZF/UNITY/FP.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/UNITY/FP.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -67,7 +67,7 @@
 by (Clarify_tac 1);
 by (dres_inst_tac [("x", "{x}")] spec 1);
 by (asm_full_simp_tac (simpset() addsimps [Int_cons_right]) 1);
-by (forward_tac [stableD2] 1);
+by (ftac stableD2 1);
 by (auto_tac (claset(), simpset() addsimps [cons_absorb, st_set_def]));
 qed "FP_Orig_subset_FP";
 

--- a/src/ZF/UNITY/GenPrefix.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/UNITY/GenPrefix.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -330,7 +330,7 @@
 \ (ALL i:nat. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))";
 by (rtac iffI 1);
 by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
-by (forward_tac [gen_prefix_length_le] 1);
+by (ftac gen_prefix_length_le 1);
 by (ALLGOALS(Clarify_tac));
 by (rtac nth_imp_gen_prefix 2);
 by (dtac (rotate_prems 4 gen_prefix_imp_nth) 1);
@@ -485,7 +485,7 @@
 by Safe_tac;
 by (Blast_tac 1);
 by (subgoal_tac "length(xs) #+ (x #- length(xs)) = x" 1);
-by (rtac (nth_drop RS ssubst) 1);
+by (stac nth_drop 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [leI])));
 by (rtac (nat_diff_split RS iffD2) 1);
 by Auto_tac;

--- a/src/ZF/UNITY/Guar.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/UNITY/Guar.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -529,7 +529,7 @@
 
 (* To be moved to WFair.ML *)
 Goal "[| F:A co A Un B; F:transient(A); st_set(B) |] ==> F:A leadsTo B";
-by (forward_tac [constrainsD2] 1);
+by (ftac constrainsD2 1);
 by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1);
 by (dres_inst_tac [("B", "A-B")] transient_strengthen 2);
 by (rtac (ensuresI RS leadsTo_Basis) 3);

--- a/src/ZF/UNITY/SubstAx.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/UNITY/SubstAx.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -70,7 +70,7 @@
 (*** Derived rules ***)
 
 Goal "F : A leadsTo B ==> F : A LeadsTo B";
-by (forward_tac [leadsToD2] 1);
+by (ftac leadsToD2 1);
 by (Clarify_tac 1);
 by (asm_simp_tac (simpset() addsimps [LeadsTo_eq]) 1);
 by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
@@ -106,7 +106,7 @@
 "[|(!!s. s:A ==> F:{s} LeadsTo B); F:program|]==>F:A LeadsTo B";
 by (cut_facts_tac [program] 1);
 by (stac (UN_singleton RS sym) 1 THEN rtac LeadsTo_UN 1);
-by (forward_tac [major] 1);
+by (ftac major 1);
 by Auto_tac;
 qed "single_LeadsTo_I";
 
@@ -209,7 +209,7 @@
 by (cut_facts_tac [minor] 1);
 by (rtac LeadsTo_Union 1);
 by (ALLGOALS(Clarify_tac));
-by (forward_tac [major] 1);
+by (ftac major 1);
 by (blast_tac (claset()  addIs [LeadsTo_weaken_R]) 1);
 qed "LeadsTo_UN_UN";
 
@@ -285,7 +285,7 @@
 
 Goal
 "[| F : A LeadsTo A'; F : B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')";
-by (rewrite_goals_tac [Unless_def]);
+by (rewtac Unless_def);
 by (dtac PSP 1);
 by (assume_tac 1);
 by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, subset_imp_LeadsTo]) 1);

--- a/src/ZF/UNITY/UNITY.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/UNITY/UNITY.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -117,7 +117,7 @@
 qed "Init_type";
 
 Goalw [st_set_def] "st_set(Init(F))";
-by (resolve_tac [Init_type] 1);
+by (rtac Init_type 1);
 qed "st_set_Init";
 AddIffs [st_set_Init];
 
@@ -439,7 +439,7 @@
 "[|(!!i. i:I ==> F:A(i) co A'(i)); F:program |]==> F:(UN i:I. A(i)) co (UN i:I. A'(i))";
 by (cut_facts_tac [minor] 1);
 by Safe_tac;
-by (ALLGOALS(forward_tac [major]));
+by (ALLGOALS(ftac major ));
 by (ALLGOALS(Asm_full_simp_tac));
 by (REPEAT(Blast_tac 1));
 qed "constrains_UN";
@@ -486,8 +486,8 @@
 by (etac not_emptyE 1);
 by Safe_tac;
 by (forw_inst_tac [("i", "xd")] major 1);
-by (forward_tac [major] 2);
-by (forward_tac [major] 3);
+by (ftac major 2);
+by (ftac major 3);
 by (REPEAT(Force_tac 1));
 qed "constrains_INT";
 

--- a/src/ZF/UNITY/Union.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/UNITY/Union.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -289,7 +289,7 @@
 by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1);
 by (Clarify_tac 1);
 by (forw_inst_tac [("i", "x")] major 1);
-by (forward_tac [constrainsD2] 1);
+by (ftac constrainsD2 1);
 by (Asm_full_simp_tac 1);
 by (blast_tac (claset() addIs [constrains_weaken]) 1);
 qed "JN_constrains_weaken";
@@ -319,10 +319,10 @@
 by (auto_tac (claset() addSIs [initially_JN_I] addDs [major], 
               simpset() addsimps [invariant_def, JN_stable]));
 by (thin_tac "i:I" 1);
-by (forward_tac [major] 1);
+by (ftac major 1);
 by (dtac major 2);
 by (auto_tac (claset(), simpset() addsimps [invariant_def]));
-by (ALLGOALS(forward_tac [stableD2]));
+by (ALLGOALS(ftac stableD2 ));
 by Auto_tac;
 qed "invariant_JN_I";
 
@@ -355,7 +355,7 @@
 by (rotate_tac ~1 3);
 by (rotate_tac ~1 1);
 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [JN_stable])));
-by (rewrite_goals_tac [st_set_def]);
+by (rewtac st_set_def);
 by (REPEAT(Blast_tac 1));
 qed "FP_JN";
 
@@ -365,7 +365,7 @@
 \  (EX i:I. programify(F(i)) : transient(A))";
 by (auto_tac (claset(),
               simpset() addsimps [transient_def, JOIN_def]));
-by (rewrite_goals_tac [st_set_def]);
+by (rewtac st_set_def);
 by (dres_inst_tac [("x", "xb")] bspec 2);
 by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
 qed "JN_transient";
@@ -566,7 +566,7 @@
 by (auto_tac (claset(), 
       simpset() addsimps [Allowed_def, 
               safety_prop_Acts_iff RS iff_sym]));  
-by (rewrite_goals_tac [safety_prop_def]);
+by (rewtac safety_prop_def);
 by Auto_tac;
 qed "safety_prop_AllowedActs_iff_Allowed";
 
@@ -579,7 +579,7 @@
                simpset() addsimps [safety_prop_def]) 2));
 by (asm_full_simp_tac (simpset() delsimps UN_simps
                    addsimps [Allowed_def, safety_prop_Acts_iff]) 1);
-by (rewrite_goals_tac [safety_prop_def]);
+by (rewtac safety_prop_def);
 by Auto_tac;
 qed "Allowed_eq";
 
@@ -628,7 +628,7 @@
 by Safe_tac;
 by (full_simp_tac (simpset() addsimps [Inter_iff]) 1);
 by (Clarify_tac 1);
-by (forward_tac [major] 1);
+by (ftac major 1);
 by (dres_inst_tac [("i", "xa")] major 2);
 by (forw_inst_tac [("i", "xa")] major 4);
 by (ALLGOALS(Asm_full_simp_tac));

--- a/src/ZF/UNITY/WFair.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/UNITY/WFair.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -243,19 +243,19 @@
 qed "leadsTo_weaken_R";
 
 Goal "[| F:A leadsTo A'; B<=A |] ==> F : B leadsTo A'";
-by (forward_tac [leadsToD2] 1);
+by (ftac leadsToD2 1);
 by (blast_tac (claset() addIs [leadsTo_Trans,subset_imp_leadsTo, st_set_subset]) 1);
 qed_spec_mp "leadsTo_weaken_L";
 
 Goal "[| F:A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F:B leadsTo B'";
-by (forward_tac [leadsToD2] 1);
+by (ftac leadsToD2 1);
 by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L, 
                                leadsTo_Trans, leadsTo_refl]) 1);
 qed "leadsTo_weaken";
 
 (* This rule has a nicer conclusion *)
 Goal "[| F:transient(A); state-A<=B; st_set(B)|] ==> F:A leadsTo B";
-by (forward_tac [transientD2] 1);
+by (ftac transientD2 1);
 by (rtac leadsTo_weaken_R 1);
 by (auto_tac (claset(), simpset() addsimps [transient_imp_leadsTo]));
 qed "transient_imp_leadsTo2";
@@ -359,7 +359,7 @@
 by (auto_tac (claset() addIs [trans_prem,union_prem], simpset()));
 by (rewrite_goal_tac [ensures_def] 1);
 by (Clarify_tac 1);
-by (forward_tac [constrainsD2] 1);
+by (ftac constrainsD2 1);
 by (dres_inst_tac [("B'", "(A-B) Un B")] constrains_weaken_R 1);
 by (Blast_tac 1);
 by (forward_tac [ensuresI2 RS leadsTo_Basis] 1);
@@ -563,7 +563,7 @@
 qed "wlt_type";
 
 Goalw [st_set_def] "st_set(wlt(F, B))";
-by (resolve_tac [wlt_type] 1);
+by (rtac wlt_type 1);
 qed "wlt_st_set";
 AddIffs [wlt_st_set];
 
@@ -575,7 +575,7 @@
 bind_thm("wlt_leadsTo", conjI RS (wlt_leadsTo_iff RS iffD2));
 
 Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt(F, B)";
-by (forward_tac [leadsToD2] 1);
+by (ftac leadsToD2 1);
 by (auto_tac (claset(), simpset() addsimps [st_set_def]));
 qed "leadsTo_subset";
 
@@ -608,7 +608,7 @@
 (* slightly different from the HOL one: B here is bounded *)
 Goal "F : A leadsTo A' \
 \     ==> EX B:Pow(state). A<=B & F:B leadsTo A' & F : (B-A') co (B Un A')";
-by (forward_tac [leadsToD2] 1);
+by (ftac leadsToD2 1);
 by (etac leadsTo_induct 1);
 (*Basis*)
 by (blast_tac (claset() addDs [ensuresD, constrainsD2, st_setD]) 1);

--- a/src/ZF/ex/Commutation.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/ex/Commutation.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -28,7 +28,7 @@
 (* A special case of square_rtrancl_on *)
 Goalw [diamond_def, commute_def, strip_def]
  "diamond(r) ==> strip(r)";
-by (resolve_tac [square_rtrancl] 1);
+by (rtac square_rtrancl 1);
 by (ALLGOALS(Asm_simp_tac));
 qed "diamond_strip";
 
@@ -116,7 +116,7 @@
 Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]  
 "confluent(r) ==> Church_Rosser(r)";
 by Auto_tac;
-by (forward_tac [fieldI1] 1);
+by (ftac fieldI1 1);
 by (full_simp_tac (simpset() addsimps [rtrancl_field]) 1);
 by (etac rtrancl_induct 1);
 by (ALLGOALS(Clarify_tac));

--- a/src/ZF/ex/Limit.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/ex/Limit.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -2317,7 +2317,7 @@
 
 val prems = Goalw [mediating_def]
   "[|emb(E,G,t);  !!n. n \\<in> nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)";
-by (Safe_tac);
+by Safe_tac;
 by (REPEAT (ares_tac prems 1));
 qed "mediatingI";
 

--- a/src/ZF/simpdata.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/ZF/simpdata.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -199,7 +199,7 @@
 qed "bex_one_point1";
 
 Goal "(EX x:A. a=x & P(x)) <-> (a:A & P(a))";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "bex_one_point2";
 
 Goal "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))";
@@ -219,7 +219,7 @@
 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
     ("EX x:A. P(x) & Q(x)",FOLogic.oT)
 
-val prove_bex_tac = rewrite_goals_tac [Bex_def] THEN
+val prove_bex_tac = rewtac Bex_def THEN
                     Quantifier1.prove_one_point_ex_tac;
 
 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
@@ -227,7 +227,7 @@
 val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
     ("ALL x:A. P(x) --> Q(x)",FOLogic.oT)
 
-val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN 
+val prove_ball_tac = rewtac Ball_def THEN 
                      Quantifier1.prove_one_point_all_tac;
 
 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;