src/HOL/ex/PiSets.ML

                  THEN (etac rule i));
 
 (* individual theorems for convenient use *)
 val [p1,p2] = goal HOL.thy "[|P == Q; P|] ==> Q";
 by (fold_goals_tac [p1]);
-br p2 1;
+by (rtac p2 1);
 val apply_def = result();
 
 goal HOL.thy "!! P x y. x = y ==> P(x) = P(y)";
-be ssubst 1;
-br refl 1;
+by (etac ssubst 1);
+by (rtac refl 1);
 val extend = result();
 
 val [p1] = goal HOL.thy "P ==> ~~P";
-br notI 1;
-br (p1 RSN(2, notE)) 1;
-ba 1;
+by (rtac notI 1);
+by (rtac (p1 RSN(2, notE)) 1);
+by (assume_tac 1);
 val notnotI = result();
 
 val [p1] = goal Set.thy "? x. x: S ==> S ~= {}";
-br contrapos 1;
-br (p1 RS notnotI) 1;
-be ssubst 1;
-br notI 1;
-be exE 1;
-be emptyE 1;
+by (rtac contrapos 1);
+by (rtac (p1 RS notnotI) 1);
+by (etac ssubst 1);
+by (rtac notI 1);
+by (etac exE 1);
+by (etac emptyE 1);
 val ExEl_NotEmpty = result();
 
 
 val [p1] = goal HOL.thy "~x ==> x = False";
 val l1 = (p1 RS (not_def RS apply_def)) RS mp;
 val l2 = read_instantiate [("P","x")] FalseE;
-br iffI 1;
-br l1 1;
-br l2 2;
-ba 1;
-ba 1;
+by (rtac iffI 1);
+by (rtac l1 1);
+by (rtac l2 2);
+by (assume_tac 1);
+by (assume_tac 1);
 val NoteqFalseEq = result();
 
 val [p1] = goal HOL.thy "~ (! x. ~P(x)) ==> ? x. P(x)";
-br exCI 1;
+by (rtac exCI 1);
 (*  1. ! x. ~ P x ==> P ?a *)
 val l1 = p1 RS NoteqFalseEq;
 (* l1 = (! x. ~ P x) = False *)
 val l2 = l1 RS iffD1;
 val l3 = l1 RS iffD2;
 val l4 = read_instantiate [("P", "P ?a")] FalseE;
-br (l2 RS l4) 1;
-ba 1;
+by (rtac (l2 RS l4) 1);
+by (assume_tac 1);
 val NotAllNot_Ex = result();
 
 val [p1] = goal HOL.thy "~(? x. P(x)) ==> ! x. ~ P(x)";
-br notnotD 1;
-br (p1 RS contrapos) 1;
-br NotAllNot_Ex 1;
-ba 1;
+by (rtac notnotD 1);
+by (rtac (p1 RS contrapos) 1);
+by (rtac NotAllNot_Ex 1);
+by (assume_tac 1);
 val NotEx_AllNot = result();
 
 goal Set.thy "!!S. ~ (? x. x : S) ==> S = {}";
 by (Fast_tac 1);
 val NoEl_Empty = result();

 by (Fast_tac 1);
 val Empty_NoElem = result();
 
 
 val [q1,q2] = goal HOL.thy "[| b = a ; (P a) |] ==> (P b)";
-br (q1 RS ssubst) 1;
-br q2 1;
+by (stac q1 1);
+by (rtac q2 1);
 val forw_subst = result();
 
 val [q1,q2] = goal HOL.thy "[| a = b ; (P a) |] ==> (P b)";
-br (q1 RS subst) 1;
-br q2 1;
+by (rtac (q1 RS subst) 1);
+by (rtac q2 1);
 val forw_ssubst = result();
 
 goal Prod.thy "((fst A),(fst(snd A)),(fst (snd (snd A))),(snd(snd(snd A)))) = A";
-br (surjective_pairing RS subst) 1;
-br (surjective_pairing RS subst) 1;
-br (surjective_pairing RS subst) 1;
-br refl 1;
+by (rtac (surjective_pairing RS subst) 1);
+by (rtac (surjective_pairing RS subst) 1);
+by (rtac (surjective_pairing RS subst) 1);
+by (rtac refl 1);
 val blow4 = result();
 
 goal Prod.thy "!! P a b. (%(a,b). P a b) A ==> P (fst A)(snd A)";
 by (Step_tac 1);
 by (afs [fst_conv,snd_conv] 1);
 val apply_pair = result();
 
 goal Prod.thy "!! P a b c d. (%(a,b,c,d). P a b c d) A \
 \ ==> P (fst A)(fst(snd A))(fst (snd (snd A)))(snd(snd(snd A)))";
-bd (blow4 RS forw_subst) 1;
+by (dtac (blow4 RS forw_subst) 1);
 by (afs [split_def] 1);
 val apply_quadr = result();
 
 goal Prod.thy "!! A B x. x: A Times B ==> x = (fst x, snd x)";
-br (surjective_pairing RS subst) 1;
-br refl 1;
+by (rtac (surjective_pairing RS subst) 1);
+by (rtac refl 1);
 val surj_pair_forw = result();
 
 goal Prod.thy "!! A B x. x: A Times B ==> fst x: A";
 by (forward_tac [surj_pair_forw] 1);
-bd forw_ssubst 1;
-ba 1;
-be SigmaD1 1;
+by (dtac forw_ssubst 1);
+by (assume_tac 1);
+by (etac SigmaD1 1);
 val TimesE1 = result();
 
 goal Prod.thy "!! A B x. x: A Times B ==> snd x: B";
 by (forward_tac [surj_pair_forw] 1);
-bd forw_ssubst 1;
-ba 1;
-be SigmaD2 1;
+by (dtac forw_ssubst 1);
+by (assume_tac 1);
+by (etac SigmaD2 1);
 val TimesE2 = result();
 
 (* -> and Pi *)
 
 goal PiSets.thy "!! A B. A -> B == {f. ! x. if x: A then f(x) : B else f(x) = (@ y. True)}";

 val funcset_def = result();
 
 
 val [q1,q2] = goal PiSets.thy 
 "[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: Pi A B";
-by (rewrite_goals_tac [Pi_def]);
-br CollectI 1;
-br allI 1;
+by (rewtac Pi_def);
+by (rtac CollectI 1);
+by (rtac allI 1);
 by (case_tac "x : A" 1);
-br (if_P RS ssubst) 1;
-ba 1;
-be q1 1;
-br (if_not_P RS ssubst) 1;
-ba 1;
-be q2 1;
+by (stac if_P 1);
+by (assume_tac 1);
+by (etac q1 1);
+by (stac if_not_P 1);
+by (assume_tac 1);
+by (etac q2 1);
 val Pi_I = result();
 
 goal PiSets.thy 
 "!! A f. [| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A -> B";
 by (afs [Pi_I] 1);

 by (afs [funcset_def] 1);
 val funcset2E1 = result();
 
 goal PiSets.thy "!! f g A B. [| f: A -> B; g: A -> B; ! x: A. f x = g x |]\
 \                  ==> f = g";
-br ext 1;
+by (rtac ext 1);
 by (case_tac "x : A" 1);
 by (Fast_tac 1);
 by (fast_tac (claset() addSDs [funcsetE2] addEs [ssubst]) 1);
 val function_extensionality = result();
 
 goal PiSets.thy "!! f g A B. [| f: Pi A B; g: Pi A B; ! x: A. f x = g x |]\
 \                  ==> f = g";
-br ext 1;
+by (rtac ext 1);
 by (case_tac "x : A" 1);
 by (Fast_tac 1);
 by (fast_tac (claset() addSDs [PiE2] addEs [ssubst]) 1);
 val Pi_extensionality = result();
 
 (* compose *)
 goal PiSets.thy "!! A B C f g. [| f: A -> B; g: B -> C |]==> compose A g f: A -> C";
-br funcsetI 1;
+by (rtac funcsetI 1);
 by (rewrite_goals_tac [compose_def,restrict_def]);  
 by (afs [funcsetE1] 1);
-br (if_not_P RS ssubst) 1;
-ba 1;
-br refl 1;
+by (stac if_not_P 1);
+by (assume_tac 1);
+by (rtac refl 1);
 val funcset_compose = result();
 
 goal PiSets.thy "!! A B C f g h. [| f: A -> B; g: B -> C; h: C -> D |]\
 \           ==> compose A h (compose A g f) = compose A (compose B h g) f";
 by (res_inst_tac [("A","A")] function_extensionality 1);
-br funcset_compose 1;
-br funcset_compose 1;
-ba 1;
-ba 1;
-ba 1;
-br funcset_compose 1;
-ba 1;
-br funcset_compose 1;
-ba 1;
-ba 1;
-br ballI 1;
+by (rtac funcset_compose 1);
+by (rtac funcset_compose 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac funcset_compose 1);
+by (assume_tac 1);
+by (rtac funcset_compose 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac ballI 1);
 by (rewrite_goals_tac [compose_def,restrict_def]);  
 by (afs [funcsetE1,if_P RS ssubst] 1);
 val compose_assoc = result();
 
 goal PiSets.thy "!! A B C f g x. [| f: A -> B; g: B -> C; x: A |]==> compose A g f x = g(f(x))";
 by (afs [compose_def, restrict_def, if_P RS ssubst] 1);
 val composeE1 = result();
 
 goal PiSets.thy "!! A B C g f.[| f : A -> B; f `` A = B; g: B -> C; g `` B = C |]\
 \                          ==> compose A g f `` A = C";
-br equalityI 1;
-br subsetI 1;
-be imageE 1;
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac imageE 1);
 by (rotate_tac 4 1);
-be ssubst 1;
-br (funcset_compose RS funcsetE1) 1;
-ba 1;
-ba 1;
-ba 1;
-br subsetI 1;
+by (etac ssubst 1);
+by (rtac (funcset_compose RS funcsetE1) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac subsetI 1);
 by (hyp_subst_tac 1);
-be imageE 1;
+by (etac imageE 1);
 by (rotate_tac 3 1);
-be ssubst 1;
-be imageE 1;
+by (etac ssubst 1);
+by (etac imageE 1);
 by (rotate_tac 3 1);
-be ssubst 1;
-be (composeE1 RS subst) 1;
-ba 1;
-ba 1;
-br imageI 1;
-ba 1;
+by (etac ssubst 1);
+by (etac (composeE1 RS subst) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac imageI 1);
+by (assume_tac 1);
 val surj_compose = result();
 
 
 goal PiSets.thy "!! A B C g f.[| f : A -> B; g: B -> C; f `` A = B; inj_on f A; inj_on g B |]\
 \                          ==> inj_on (compose A g f) A";
-br inj_onI 1;
+by (rtac inj_onI 1);
 by (forward_tac [composeE1] 1);
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
 by (forward_tac [composeE1] 1);
-ba 1;
+by (assume_tac 1);
 by (rotate_tac 7 1);
-ba 1;
+by (assume_tac 1);
 by (step_tac (claset() addSEs [inj_onD]) 1);
 by (rotate_tac 5 1);
-be subst 1;
-be subst 1;
-ba 1;
-be imageI 1;
-be imageI 1;
+by (etac subst 1);
+by (etac subst 1);
+by (assume_tac 1);
+by (etac imageI 1);
+by (etac imageI 1);
 val inj_on_compose = result();
 
 
 (* restrict / lam *)
 goal PiSets.thy "!! f A B. [| f `` A <= B |] ==> (lam x: A. f x) : A -> B";
-by (rewrite_goals_tac [restrict_def]);
-br funcsetI 1;
+by (rewtac restrict_def);
+by (rtac funcsetI 1);
 by (afs [if_P RS ssubst] 1);
-be subsetD 1;
-be imageI 1;
+by (etac subsetD 1);
+by (etac imageI 1);
 by (afs [if_not_P RS ssubst] 1);
 val restrict_in_funcset = result();
 
 goal PiSets.thy "!! f A B. [| ! x: A. f x: B |] ==> (lam x: A. f x) : A -> B";
-br restrict_in_funcset 1;
+by (rtac restrict_in_funcset 1);
 by (afs [image_def] 1);
 by (Step_tac 1);
 by (Fast_tac 1);
 val restrictI = result();
 
 goal PiSets.thy "!! f A B. [| ! x: A. f x: B x |] ==> (lam x: A. f x) : Pi A B";
-by (rewrite_goals_tac [restrict_def]);
-br Pi_I 1;
+by (rewtac restrict_def);
+by (rtac Pi_I 1);
 by (afs [if_P RS ssubst] 1);
 by (Asm_full_simp_tac 1);
 val restrictI_Pi = result();
 
 (* The following proof has to be redone *)
 goal PiSets.thy "!! f A B C.[| f `` A  <= B -> C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C";
-br restrict_in_funcset 1;
+by (rtac restrict_in_funcset 1);
 by (afs [image_def] 1);
 by (afs [Pi_def,subset_def] 1);
 by (afs [restrict_def] 1);
 by (Step_tac 1);
 by (Asm_full_simp_tac 1);
 by (dres_inst_tac [("x","f xa")] spec 1);
-bd mp 1;
-br bexI 1;
-br refl 1;
-ba 1;
+by (dtac mp 1);
+by (rtac bexI 1);
+by (rtac refl 1);
+by (assume_tac 1);
 by (dres_inst_tac [("x","xb")] spec 1);
 by (Asm_full_simp_tac 1);
 (* fini 1 *)
 by (Asm_full_simp_tac 1);
 val restrict_in_funcset2 = result();
 
 goal PiSets.thy "!! f A B C.[| !x: A. ! y: B. f x y: C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C";
-br restrict_in_funcset 1;
+by (rtac restrict_in_funcset 1);
 by (afs [image_def] 1);
 by (afs [Pi_def,subset_def] 1);
 by (afs [restrict_def] 1);
 by (Step_tac 1);
 by (Asm_full_simp_tac 1);

 val restrict2E2 = result();
 
 
 goal PiSets.thy "!! f g A B. [| ! x: A. f x = g x |]\
 \                             ==> (lam x: A. f x) = (lam x: A. g x)";
-br ext 1;
+by (rtac ext 1);
 by (case_tac "x: A" 1);
 by (afs [restrictE1] 1);
 by (afs [restrictE2] 1);
 val restrict_ext = result();
 
 (* Invers *)
 
 goal PiSets.thy "!! f A B.[|f `` A = B; x: B |] ==> ? y: A. f y = x";
-by (rewrite_goals_tac [image_def]);
-bd equalityD2 1;
-bd subsetD 1;
-ba 1;
-bd CollectD 1;
-be bexE 1;
-bd sym 1;
-be bexI 1;
-ba 1;
+by (rewtac image_def);
+by (dtac equalityD2 1);
+by (dtac subsetD 1);
+by (assume_tac 1);
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (dtac sym 1);
+by (etac bexI 1);
+by (assume_tac 1);
 val surj_image = result();
 
 val [q1,q2] = goal PiSets.thy "[| f `` A = B; f : A -> B |] \
 \             ==> (lam x: B. (Inv A f) x) : B -> A";
-br restrict_in_funcset 1;
-by (rewrite_goals_tac [image_def]);
-br subsetI 1; 
-bd CollectD 1;
-be bexE 1;
-be ssubst 1;
-bd (q1 RS surj_image) 1;
-be bexE 1;
-be subst 1;
-by (rewrite_goals_tac [Inv_def]);
+by (rtac restrict_in_funcset 1);
+by (rewtac image_def);
+by (rtac subsetI 1); 
+by (dtac CollectD 1);
+by (etac bexE 1);
+by (etac ssubst 1);
+by (dtac (q1 RS surj_image) 1);
+by (etac bexE 1);
+by (etac subst 1);
+by (rewtac Inv_def);
 by (res_inst_tac [("Q","f(@ ya. ya : A & f ya = f y) = f y")] conjunct1 1);
-br (q1 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
-be (q2 RS funcsetE1) 1;
+by (rtac (q1 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
+by (etac (q2 RS funcsetE1) 1);
 val Inv_funcset = result();
 
 
 val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\
 \                ==> ! x: A. (lam y: B. (Inv A f) y)(f x) = x";
-br ballI 1;
-br (restrictE1 RS ssubst) 1;
-be (q1 RS funcsetE1) 1;
-by (rewrite_goals_tac [Inv_def]); 
-br (q2 RS inj_onD) 1;
-ba 3;
+by (rtac ballI 1);
+by (stac restrictE1 1);
+by (etac (q1 RS funcsetE1) 1);
+by (rewtac Inv_def); 
+by (rtac (q2 RS inj_onD) 1);
+by (assume_tac 3);
 by (res_inst_tac [("P","(@ y. y : A & f y = f x) : A")] conjunct2 1);
-br (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
-be (q1 RS funcsetE1) 1;
+by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
+by (etac (q1 RS funcsetE1) 1);
 by (res_inst_tac [("Q","f (@ y. y : A & f y = f x) = f x")] conjunct1 1);
-br (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
-be (q1 RS funcsetE1) 1;
+by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
+by (etac (q1 RS funcsetE1) 1);
 val Inv_f_f = result();
 
 val [q1,q2] = goal PiSets.thy "[| f: A -> B; f `` A = B |]\
 \                ==> ! x: B. f ((lam y: B. (Inv A f y)) x) = x";
-br ballI 1;
-br (restrictE1 RS ssubst) 1;
-ba 1;
-by (rewrite_goals_tac [Inv_def]); 
+by (rtac ballI 1);
+by (stac restrictE1 1);
+by (assume_tac 1);
+by (rewtac Inv_def); 
 by (res_inst_tac [("P","(@ y. y : A & f y = x) : A")] conjunct2 1);
-br (q2 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1;
-ba 1;
+by (rtac (q2 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
+by (assume_tac 1);
 val f_Inv_f = result();
 
 val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\
 \                ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
-br function_extensionality 1;
-br funcset_compose 1;
-br q1 1;
-br (q1 RS (q3 RS Inv_funcset)) 1;
-br restrict_in_funcset 1;
-by (Fast_tac 1);
-br ballI 1;
+by (rtac function_extensionality 1);
+by (rtac funcset_compose 1);
+by (rtac q1 1);
+by (rtac (q1 RS (q3 RS Inv_funcset)) 1);
+by (rtac restrict_in_funcset 1);
+by (Fast_tac 1);
+by (rtac ballI 1);
 by (afs [compose_def] 1);
-br (restrictE1 RS ssubst) 1;
-ba 1;
-br (restrictE1 RS ssubst) 1;
-ba 1;
-be (q3 RS (q2 RS (q1 RS Inv_f_f)) RS bspec) 1;
+by (stac restrictE1 1);
+by (assume_tac 1);
+by (stac restrictE1 1);
+by (assume_tac 1);
+by (etac (q3 RS (q2 RS (q1 RS Inv_f_f)) RS bspec) 1);
 val comp_Inv_id = result();
 
 
 (* Pi and its application @@ *)
 
 goal PiSets.thy "!! A B. (PI x: A. B x) ~= {} ==> ! x: A. B(x) ~= {}";
-bd NotEmpty_ExEl 1;
-be exE 1;
-by (rewrite_goals_tac [Pi_def]);
-bd CollectD 1;
-br ballI 1;
-br ExEl_NotEmpty 1;
+by (dtac NotEmpty_ExEl 1);
+by (etac exE 1);
+by (rewtac Pi_def);
+by (dtac CollectD 1);
+by (rtac ballI 1);
+by (rtac ExEl_NotEmpty 1);
 by (res_inst_tac [("x","x xa")] exI 1);
 by (afs [if_P RS subst] 1);
 val Pi_total1 = result();
 
 goal Set.thy "!! M P. ? x: M . P x ==> (~ (! x: M. ~ P x))";
 by (Fast_tac 1);
 val SetEx_NotNotAll = result();
 
 goal PiSets.thy "!! A B. ? x: A. B(x) = {} ==> (PI x: A. B x) = {}";
-br notnotD 1;
-br (Pi_total1 RSN(2,contrapos)) 1;
-ba 2; 
-be SetEx_NotNotAll 1;
+by (rtac notnotD 1);
+by (rtac (Pi_total1 RSN(2,contrapos)) 1);
+by (assume_tac 2); 
+by (etac SetEx_NotNotAll 1);
 val Pi_total2 = result();
 
 val [q1,q2] = goal PiSets.thy "[|a : A; Pi A B ~= {} |] ==> (Pi A B) @@ a = B(a)";
-by (rewrite_goals_tac [Fset_apply_def]);
-br equalityI 1;
-br subsetI 1;
-be imageE 1;
-be ssubst 1;
-by (rewrite_goals_tac [Pi_def]);
-bd CollectD 1;
-bd spec 1;
-br (q1 RS if_P RS subst) 1;  
-ba 1;
-br subsetI 1;
-by (rewrite_goals_tac [image_def]);
-br CollectI 1;
-br exE 1;
-br (q2 RS NotEmpty_ExEl) 1;
+by (rewtac Fset_apply_def);
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac imageE 1);
+by (etac ssubst 1);
+by (rewtac Pi_def);
+by (dtac CollectD 1);
+by (dtac spec 1);
+by (rtac (q1 RS if_P RS subst) 1);  
+by (assume_tac 1);
+by (rtac subsetI 1);
+by (rewtac image_def);
+by (rtac CollectI 1);
+by (rtac exE 1);
+by (rtac (q2 RS NotEmpty_ExEl) 1);
 by (res_inst_tac [("x","%y. if  (y = a) then  x else xa y")] bexI 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
-br allI 1;
+by (rtac allI 1);
 by (case_tac "xb: A" 1);
 by (afs [if_P RS ssubst] 1);
 by (case_tac "xb = a" 1);
 by (afs [if_P RS ssubst] 1);
 by (afs [if_not_P RS ssubst] 1);
-by (rewrite_goals_tac [Pi_def]);
+by (rewtac Pi_def);
 by (afs [if_P RS ssubst] 1);
 by (afs [if_not_P RS ssubst] 1);
 by (case_tac "xb = a" 1);
 by (afs [if_P RS ssubst] 1);
 by (hyp_subst_tac 1);
 by (afs [q1] 1);
 by (afs [if_not_P RS ssubst] 1);
 val Pi_app_def = result();
 
 goal PiSets.thy "!! a A B C. [| a: A; (PI x: A. PI y: B x. C x y) ~= {} |] ==>  (PI y: B a. C a y) ~= {}";
-bd NotEmpty_ExEl 1;
-be exE 1;
-by (rewrite_goals_tac [Pi_def]);
-bd CollectD 1;
-bd spec 1;
-br ExEl_NotEmpty 1;
-br exI 1;
-be (if_P RS eq_reflection RS apply_def) 1;
-ba 1;
+by (dtac NotEmpty_ExEl 1);
+by (etac exE 1);
+by (rewtac Pi_def);
+by (dtac CollectD 1);
+by (dtac spec 1);
+by (rtac ExEl_NotEmpty 1);
+by (rtac exI 1);
+by (etac (if_P RS eq_reflection RS apply_def) 1);
+by (assume_tac 1);
 val NotEmptyPiStep = result();
 
 val [q1,q2,q3] = goal PiSets.thy 
 "[|a : A; b: B a; (PI x: A. PI y: B x. C x y) ~= {} |] ==> (PI x: A. PI y: B x. C x y) @@ a @@ b = C a b";
 by (fold_goals_tac [q3 RS (q1 RS NotEmptyPiStep) RS (q2 RS Pi_app_def) RS eq_reflection]);
 by (fold_goals_tac [q3 RS (q1 RS Pi_app_def) RS eq_reflection]);
-br refl 1;
+by (rtac refl 1);
 val Pi_app2_def = result();
 
 (* Sigma does a better job ( the following is from PiSig.ML) *)
 goal PiSets.thy "!! A b a. [| a: A; Pi A B ~= {} |]\
 \ ==>  Sigma A B ^^ {a} = Pi A B @@ a";
-br (Pi_app_def RS ssubst) 1;
-ba 1;
-ba 1;
+by (stac Pi_app_def 1);
+by (assume_tac 1);
+by (assume_tac 1);
 by (afs [Sigma_def,Domain_def,converse_def,Range_def,Image_def] 1);
-by (rewrite_goals_tac [Bex_def]);
+by (rewtac Bex_def);
 by (Fast_tac 1);
 val PiSig_image_eq = result();
 
 goal PiSets.thy "!! A b a. [| a: A |]\
 \ ==>  Sigma A B ^^ {a} = B a";

 val Sigma_app_def = result();
 
 (* Bijection between Pi in terms of => and Pi in terms of Sigma *)
 goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f <= Sigma A B";
 by (afs [PiBij_def,Pi_def,restrictE1] 1);
-br subsetI 1;
+by (rtac subsetI 1);
 by (split_all_tac 1);
-bd CollectD 1;
+by (dtac CollectD 1);
 by (Asm_full_simp_tac 1);
 val PiBij_subset_Sigma = result();
 
 goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";
 by (afs [PiBij_def,restrictE1] 1);
-br ballI 1;
-br ex1I 1;
-ba 2;
-br refl 1;
+by (rtac ballI 1);
+by (rtac ex1I 1);
+by (assume_tac 2);
+by (rtac refl 1);
 val PiBij_unique = result();
 
 goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. y: B x & (x, y): (PiBij A B f)))";
 by (afs [PiBij_def,restrictE1] 1);
-br ballI 1;
-br ex1I 1;
-be conjunct2 2;
+by (rtac ballI 1);
+by (rtac ex1I 1);
+by (etac conjunct2 2);
 by (afs [PiE1] 1);
 val PiBij_unique2 = result();
 
 goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f : Graph A B";
 by (afs [Graph_def,PiBij_unique,PiBij_subset_Sigma] 1);
 val PiBij_in_Graph = result();
 
 goal PiSets.thy "!! A B. PiBij A B:  Pi A B -> Graph A B";
 by (afs [PiBij_def] 1);
-br restrictI 1;
+by (rtac restrictI 1);
 by (strip 1);
 by (afs [Graph_def] 1);
-br conjI 1;
-br subsetI 1;
+by (rtac conjI 1);
+by (rtac subsetI 1);
 by (strip 2);
-br ex1I 2;
-br refl 2;
-ba 2;
+by (rtac ex1I 2);
+by (rtac refl 2);
+by (assume_tac 2);
 by (split_all_tac 1);
 by (afs [Pi_def] 1);
 val PiBij_func = result();
 
 goal PiSets.thy "!! A f g x. [| f: Pi A B; g: Pi A B;  \
 \       {(x, y). x: A & y = f x} = {(x, y). x: A & y = g x}; x: A |]\
 \                ==> f x = g x";
-be equalityE 1;
-by (rewrite_goals_tac [subset_def]);
+by (etac equalityE 1);
+by (rewtac subset_def);
 by (dres_inst_tac [("x","(x, f x)")] bspec 1);
 by (Fast_tac 1);
 by (Fast_tac 1);
 val set_eq_lemma = result();
 
 goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)";
-br inj_onI 1;
-br Pi_extensionality 1;			
-ba 1;
-ba 1;
+by (rtac inj_onI 1);
+by (rtac Pi_extensionality 1);			
+by (assume_tac 1);
+by (assume_tac 1);
 by (strip 1);
 by (afs [PiBij_def,restrictE1] 1);
 by (re_tac set_eq_lemma 2 1);
-ba 1;
-ba 2;
+by (assume_tac 1);
+by (assume_tac 2);
 by (afs [restrictE1] 1);
-be subst 1;
+by (etac subst 1);
 by (afs [restrictE1] 1);
 val inj_PiBij = result();
 
 goal HOL.thy "!! P . ?! x. P x ==> ? x. P x";
 by (Blast_tac 1);
 val Ex1_Ex = result();
 
 goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B";
-br equalityI 1;
+by (rtac equalityI 1);
 by (afs [image_def] 1);
-br subsetI 1;
-by (Asm_full_simp_tac 1);
-be bexE 1;
-be ssubst 1;
+by (rtac subsetI 1);
+by (Asm_full_simp_tac 1);
+by (etac bexE 1);
+by (etac ssubst 1);
 by (afs [PiBij_in_Graph] 1);
-br subsetI 1;
+by (rtac subsetI 1);
 by (afs [image_def] 1);
 by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);
-br restrictI_Pi 2;
+by (rtac restrictI_Pi 2);
 by (strip 2);
-br ex1E 2;
+by (rtac ex1E 2);
 by (afs [Graph_def] 2);
-be conjE 2;
-bd bspec 2;
-ba 2;
-ba 2;
-br (select_equality RS ssubst) 2;
-ba 2;
+by (etac conjE 2);
+by (dtac bspec 2);
+by (assume_tac 2);
+by (assume_tac 2);
+by (stac select_equality 2);
+by (assume_tac 2);
 by (Blast_tac 2);
 (* gets hung up on by (afs [Graph_def] 2); *)
-by (SELECT_GOAL (rewrite_goals_tac [Graph_def]) 2);
+by (SELECT_GOAL (rewtac Graph_def) 2);
 by (Blast_tac 2);
 (* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
 by (afs [PiBij_def,Graph_def] 1);
-br (restrictE1 RS ssubst) 1;
-br restrictI_Pi 1;
+by (stac restrictE1 1);
+by (rtac restrictI_Pi 1);
 (* again like the old 2. subgoal *)
 by (strip 1);
-br ex1E 1;
-be conjE 1;
-bd bspec 1;
-ba 1;
-ba 1;
-br (select_equality RS ssubst) 1;
-ba 1;
+by (rtac ex1E 1);
+by (etac conjE 1);
+by (dtac bspec 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (stac select_equality 1);
+by (assume_tac 1);
 by (Blast_tac 1);
 by (Blast_tac 1);
 (* *)
-br equalityI 1;
-br subsetI 1;
-br CollectI 1;
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (rtac CollectI 1);
 by (split_all_tac 1);
 by (Simp_tac 1);
-br conjI 1;
+by (rtac conjI 1);
 by (Blast_tac 1);
-be conjE 1;
-bd subsetD 1;
-ba 1;
-bd SigmaD1 1;
-bd bspec 1;
-ba 1;
-br (restrictE1 RS ssubst) 1;
-ba 1;
-br sym 1;
-br select_equality 1;
-ba 1;
+by (etac conjE 1);
+by (dtac subsetD 1);
+by (assume_tac 1);
+by (dtac SigmaD1 1);
+by (dtac bspec 1);
+by (assume_tac 1);
+by (stac restrictE1 1);
+by (assume_tac 1);
+by (rtac sym 1);
+by (rtac select_equality 1);
+by (assume_tac 1);
 by (Blast_tac 1);
 (* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x   *)
-br subsetI 1;
+by (rtac subsetI 1);
 by (Asm_full_simp_tac 1);
 by (split_all_tac 1);
 by (Asm_full_simp_tac 1);
-be conjE 1;
-be conjE 1;
+by (etac conjE 1);
+by (etac conjE 1);
 by (afs [restrictE1] 1);
-bd bspec 1;
-ba 1;
-bd Ex1_Ex 1;
-by (rewrite_goals_tac [Ex_def]);
-ba 1;
+by (dtac bspec 1);
+by (assume_tac 1);
+by (dtac Ex1_Ex 1);
+by (rewtac Ex_def);
+by (assume_tac 1);
 val surj_PiBij = result();
 
 
 goal PiSets.thy "!! A B. [| f: Pi A B |] ==> \
 \ (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";
-br (Inv_f_f  RS bspec) 1;
-ba 4;
+by (rtac (Inv_f_f  RS bspec) 1);
+by (assume_tac 4);
 by (afs [PiBij_func] 1);
 by (afs [inj_PiBij] 1);
 by (afs [surj_PiBij] 1);
 val PiBij_bij1 = result();
 
 goal PiSets.thy "!! A B. [| f: Graph A B  |] ==> \
 \    (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f";
-br (PiBij_func RS (f_Inv_f RS bspec)) 1;
+by (rtac (PiBij_func RS (f_Inv_f RS bspec)) 1);
 by (afs [surj_PiBij] 1);
-ba 1;
+by (assume_tac 1);
 val PiBij_bij2 = result();
 
 goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> inj f";
-br injI 1;
+by (rtac injI 1);
 by (dres_inst_tac [("f","g")] arg_cong 1);
 by (forw_inst_tac [("x","x")] spec 1);
 by (rotate_tac 2 1);
-be subst 1;
+by (etac subst 1);
 by (forw_inst_tac [("x","y")] spec 1);
 by (rotate_tac 2 1);
-be subst 1;
-ba 1;
+by (etac subst 1);
+by (assume_tac 1);
 val inj_lemma = result();
 
 goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> surj g";
 by (afs [surj_def] 1);
-br allI 1;
+by (rtac allI 1);
 by (res_inst_tac [("x","f y")] exI 1);
-bd spec 1;
-be sym 1;
+by (dtac spec 1);
+by (etac sym 1);
 val surj_lemma = result();
 
 goal PiSets.thy "Pi {} B == {f. !x. f x = (@ y. True)}";
 by (afs [Pi_def] 1);
 val empty_Pi = result();

 by (Blast_tac 1);
 val subsetND = result();
 
 
 goal PiSets.thy "!! A B C . [| ! x: A. B x <= C x |] ==> Pi A B <= Pi A C";
-br subsetI 1;
-br Pi_I 1;
+by (rtac subsetI 1);
+by (rtac Pi_I 1);
 by (afs [Pi_def] 2);
-bd bspec 1;
-ba 1;
-be subsetD 1;
+by (dtac bspec 1);
+by (assume_tac 1);
+by (etac subsetD 1);
 by (afs [PiE1] 1);
 val Pi_subset1 = result();