CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
CCL/CCL, Fix, Gfp, Hered, Set, Term, Trancl, Type, Wfd: expanded shorthands

--- a/src/CCL/CCL.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/CCL.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -44,11 +44,11 @@
 (*** Termination and Divergence ***)
 
 goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot";
-br iff_refl 1;
+by (rtac iff_refl 1);
 val Trm_iff = result();
 
 goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <-> t = bot";
-br iff_refl 1;
+by (rtac iff_refl 1);
 val Dvg_iff = result();
 
 (*** Constructors are injective ***)
@@ -138,7 +138,7 @@
 (****** Facts from gfp Definition of [= and = ******)
 
 val major::prems = goal Set.thy "[| A=B;  a:B <-> P |] ==> a:A <-> P";
-brs (prems RL [major RS ssubst]) 1;
+by (resolve_tac (prems RL [major RS ssubst]) 1);
 val XHlemma1 = result();
 
 goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p.EX t t'.p=<t,t'> &  P(t,t')} <-> Q)";
@@ -148,7 +148,7 @@
 (*** Pre-Order ***)
 
 goalw CCL.thy [POgen_def,SIM_def]  "mono(%X.POgen(X))";
-br monoI 1;
+by (rtac monoI 1);
 by (safe_tac ccl_cs);
 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
 by (ALLGOALS (simp_tac ccl_ss));
@@ -159,7 +159,7 @@
   "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
 \                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
 \                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
-br (iff_refl RS XHlemma2) 1;
+by (rtac (iff_refl RS XHlemma2) 1);
 val POgenXH = result();
 
 goal CCL.thy
@@ -169,29 +169,29 @@
 by (simp_tac (ccl_ss addsimps [PO_iff]) 1);
 br (rewrite_rule [POgen_def,SIM_def] 
                  (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
-br (iff_refl RS XHlemma2) 1;
+by (rtac (iff_refl RS XHlemma2) 1);
 val poXH = result();
 
 goal CCL.thy "bot [= b";
-br (poXH RS iffD2) 1;
+by (rtac (poXH RS iffD2) 1);
 by (simp_tac ccl_ss 1);
 val po_bot = result();
 
 goal CCL.thy "a [= bot --> a=bot";
-br impI 1;
-bd (poXH RS iffD1) 1;
-be rev_mp 1;
+by (rtac impI 1);
+by (dtac (poXH RS iffD1) 1);
+by (etac rev_mp 1);
 by (simp_tac ccl_ss 1);
 val bot_poleast = result() RS mp;
 
 goal CCL.thy "<a,b> [= <a',b'> <->  a [= a' & b [= b'";
-br (poXH RS iff_trans) 1;
+by (rtac (poXH RS iff_trans) 1);
 by (simp_tac ccl_ss 1);
 by (fast_tac ccl_cs 1);
 val po_pair = result();
 
 goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))";
-br (poXH RS iff_trans) 1;
+by (rtac (poXH RS iff_trans) 1);
 by (simp_tac ccl_ss 1);
 by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
 by (asm_simp_tac ccl_ss 1);
@@ -203,13 +203,13 @@
 val [p1,p2,p3,p4,p5] = goal CCL.thy
     "[| t [= t';  a [= a';  b [= b';  !!x y.c(x,y) [= c'(x,y); \
 \       !!u.d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
-br (p1 RS po_cong RS po_trans) 1;
-br (p2 RS po_cong RS po_trans) 1;
-br (p3 RS po_cong RS po_trans) 1;
-br (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1;
+by (rtac (p1 RS po_cong RS po_trans) 1);
+by (rtac (p2 RS po_cong RS po_trans) 1);
+by (rtac (p3 RS po_cong RS po_trans) 1);
+by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1);
 by (res_inst_tac [("f1","%d.case(t',a',b',c',d)")] 
                (p5 RS po_abstractn RS po_cong RS po_trans) 1);
-br po_refl 1;
+by (rtac po_refl 1);
 val case_pocong = result();
 
 val [p1,p2] = goalw CCL.thy ccl_data_defs
@@ -219,29 +219,29 @@
 
 
 val prems = goal CCL.thy "~ lam x.b(x) [= bot";
-br notI 1;
-bd bot_poleast 1;
-be (distinctness RS notE) 1;
+by (rtac notI 1);
+by (dtac bot_poleast 1);
+by (etac (distinctness RS notE) 1);
 val npo_lam_bot = result();
 
 val eq1::eq2::prems = goal CCL.thy
     "[| x=a;  y=b;  x[=y |] ==> a[=b";
-br (eq1 RS subst) 1;
-br (eq2 RS subst) 1;
-brs prems 1;
+by (rtac (eq1 RS subst) 1);
+by (rtac (eq2 RS subst) 1);
+by (resolve_tac prems 1);
 val po_lemma = result();
 
 goal CCL.thy "~ <a,b> [= lam x.f(x)";
-br notI 1;
-br (npo_lam_bot RS notE) 1;
-be (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1;
+by (rtac notI 1);
+by (rtac (npo_lam_bot RS notE) 1);
+by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
 val npo_pair_lam = result();
 
 goal CCL.thy "~ lam x.f(x) [= <a,b>";
-br notI 1;
-br (npo_lam_bot RS notE) 1;
-be (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1;
+by (rtac notI 1);
+by (rtac (npo_lam_bot RS notE) 1);
+by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
 val npo_lam_pair = result();
 
@@ -260,7 +260,7 @@
 (* Coinduction for [= *)
 
 val prems = goal CCL.thy "[|  <t,u> : R;  R <= POgen(R) |] ==> t [= u";
-br (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1;
+by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1);
 by (REPEAT (ares_tac prems 1));
 val po_coinduct = result();
 
@@ -269,7 +269,7 @@
 (*************** EQUALITY *******************)
 
 goalw CCL.thy [EQgen_def,SIM_def]  "mono(%X.EQgen(X))";
-br monoI 1;
+by (rtac monoI 1);
 by (safe_tac set_cs);
 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
 by (ALLGOALS (simp_tac ccl_ss));
@@ -281,7 +281,7 @@
 \                                            (t=false & t'=false) | \
 \                (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
 \                (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
-br (iff_refl RS XHlemma2) 1;
+by (rtac (iff_refl RS XHlemma2) 1);
 val EQgenXH = result();
 
 goal CCL.thy
@@ -292,21 +292,21 @@
   "<t,t'> : EQ <-> (t=bot & t'=bot)  | (t=true & t'=true) | (t=false & t'=false) | \
 \             (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : EQ & <b,b'> : EQ) | \
 \             (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : EQ))" 1);
-be rev_mp 1;
+by (etac rev_mp 1);
 by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
 br (rewrite_rule [EQgen_def,SIM_def]
                  (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
-br (iff_refl RS XHlemma2) 1;
+by (rtac (iff_refl RS XHlemma2) 1);
 val eqXH = result();
 
 val prems = goal CCL.thy "[|  <t,u> : R;  R <= EQgen(R) |] ==> t = u";
-br (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1;
+by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1);
 by (REPEAT (ares_tac prems 1));
 val eq_coinduct = result();
 
 val prems = goal CCL.thy 
     "[|  <t,u> : R;  R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u";
-br (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1;
+by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1);
 by (REPEAT (ares_tac (EQgen_mono::prems) 1));
 val eq_coinduct3 = result();
 

--- a/src/CCL/Fix.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/Fix.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -12,7 +12,7 @@
 
 val [base,step,incl] = goalw Fix.thy [INCL_def]
     "[| P(bot);  !!x.P(x) ==> P(f(x));  INCL(P) |] ==> P(fix(f))";
-br (incl RS spec RS mp) 1;
+by (rtac (incl RS spec RS mp) 1);
 by (rtac (Nat_ind RS ballI) 1 THEN atac 1);
 by (ALLGOALS (simp_tac term_ss));
 by (REPEAT (ares_tac [base,step] 1));
@@ -22,7 +22,7 @@
 
 val prems = goalw Fix.thy [INCL_def]
      "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))";
-br iff_refl 1;
+by (rtac iff_refl 1);
 val inclXH = result();
 
 val prems = goal Fix.thy
@@ -45,13 +45,13 @@
 (*** Lemmas for Inclusive Predicates ***)
 
 goal Fix.thy "INCL(%x.~ a(x) [= t)";
-br inclI 1;
-bd bspec 1;
-br zeroT 1;
-be contrapos 1;
-br po_trans 1;
-ba 2;
-br (napplyBzero RS ssubst) 1;
+by (rtac inclI 1);
+by (dtac bspec 1);
+by (rtac zeroT 1);
+by (etac contrapos 1);
+by (rtac po_trans 1);
+by (assume_tac 2);
+by (rtac (napplyBzero RS ssubst) 1);
 by (rtac po_cong 1 THEN rtac po_bot 1);
 val npo_INCL = result();
 
@@ -77,21 +77,21 @@
 (* Fixed points of idgen *)
 
 goal Fix.thy "idgen(fix(idgen)) = fix(idgen)";
-br (fixB RS sym) 1;
+by (rtac (fixB RS sym) 1);
 val fix_idgenfp = result();
 
 goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x";
 by (simp_tac term_ss 1);
-br (term_case RS allI) 1;
+by (rtac (term_case RS allI) 1);
 by (ALLGOALS (simp_tac term_ss));
 val id_idgenfp = result();
 
 (* All fixed points are lam-expressions *)
 
 val [prem] = goal Fix.thy "idgen(d) = d ==> d = lam x.?f(x)";
-br (prem RS subst) 1;
-bw idgen_def;
-br refl 1;
+by (rtac (prem RS subst) 1);
+by (rewtac idgen_def);
+by (rtac refl 1);
 val idgenfp_lam = result();
 
 (* Lemmas for rewriting fixed points of idgen *)
@@ -117,14 +117,14 @@
 
 val [p1,p2,p3] = goal CCL.thy
     "[| ALL x.t ` x [= u ` x;  EX f.t=lam x.f(x);  EX f.u=lam x.f(x) |] ==> t [= u";
-br (p2 RS cond_eta RS ssubst) 1;
-br (p3 RS cond_eta RS ssubst) 1;
-br (p1 RS (po_lam RS iffD2)) 1;
+by (rtac (p2 RS cond_eta RS ssubst) 1);
+by (rtac (p3 RS cond_eta RS ssubst) 1);
+by (rtac (p1 RS (po_lam RS iffD2)) 1);
 val po_eta = result();
 
 val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)";
-br (prem RS subst) 1;
-br refl 1;
+by (rtac (prem RS subst) 1);
+by (rtac refl 1);
 val po_eta_lemma = result();
 
 val [prem] = goal Fix.thy
@@ -139,8 +139,8 @@
 
 val [prem] = goal Fix.thy
     "idgen(d) = d ==> fix(idgen) [= d";
-br (allI RS po_eta) 1;
-br (lemma1 RSN(2,po_coinduct)) 1;
+by (rtac (allI RS po_eta) 1);
+by (rtac (lemma1 RSN(2,po_coinduct)) 1);
 by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
 val fix_least_idgen = result();
 
@@ -155,8 +155,8 @@
 
 val [prem] = goal Fix.thy
     "idgen(d) = d ==> lam x.x [= d";
-br (allI RS po_eta) 1;
-br (lemma2 RSN(2,po_coinduct)) 1;
+by (rtac (allI RS po_eta) 1);
+by (rtac (lemma2 RSN(2,po_coinduct)) 1);
 by (simp_tac term_ss 1);
 by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
 val id_least_idgen = result();
@@ -170,8 +170,8 @@
 (********)
 
 val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t";
-br (prem RS sym RS subst) 1;
-br applyB 1;
+by (rtac (prem RS sym RS subst) 1);
+by (rtac applyB 1);
 val id_apply = result();
 
 val prems = goal Fix.thy
@@ -179,13 +179,13 @@
 \        !!x y.[| P(x);  P(y) |] ==> P(<x,y>);  \
 \        !!u.(!!x.P(u(x))) ==> P(lam x.u(x));  INCL(P) |] ==> \
 \     P(t)";
-br (reachability RS id_apply RS subst) 1;
+by (rtac (reachability RS id_apply RS subst) 1);
 by (res_inst_tac [("x","t")] spec 1);
-br fix_ind 1;
-bw idgen_def;
+by (rtac fix_ind 1);
+by (rewtac idgen_def);
 by (REPEAT_SOME (ares_tac [allI]));
-br (applyBbot RS ssubst) 1;
-brs prems 1;
+by (rtac (applyBbot RS ssubst) 1);
+by (resolve_tac prems 1);
 br (applyB RS ssubst )1;
 by (res_inst_tac [("t","xa")] term_case 1);
 by (ALLGOALS (simp_tac term_ss));

--- a/src/CCL/Gfp.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/Gfp.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -60,10 +60,11 @@
 val coinduct2_lemma = result();
 
 (*strong version, thanks to Martin Coen*)
-val prems = goal Gfp.thy
+val ainA::prems = goal Gfp.thy
     "[| a: A;  A <= f(A) Un gfp(f);  mono(f) |] ==> a : gfp(f)";
-by (rtac (coinduct2_lemma RSN (2,coinduct)) 1);
-by (REPEAT (resolve_tac (prems@[UnI1]) 1));
+by (rtac coinduct 1);
+by (rtac (prems MRS coinduct2_lemma) 2);
+by (resolve_tac [ainA RS UnI1] 1);
 val coinduct2 = result();
 
 (***  Even Stronger version of coinduct  [by Martin Coen]
@@ -78,22 +79,22 @@
     "[| A <= f(lfp(%x.f(x) Un A Un gfp(f)));  mono(f) |] ==> \
 \    lfp(%x.f(x) Un A Un gfp(f)) <= f(lfp(%x.f(x) Un A Un gfp(f)))";
 by (rtac subset_trans 1);
-br (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1;
+by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1);
 by (rtac (Un_least RS Un_least) 1);
-br subset_refl 1;
-br prem 1;
-br (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1;
+by (rtac subset_refl 1);
+by (rtac prem 1);
+by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1);
 by (rtac (mono RS monoD) 1);
 by (rtac (mono RS coinduct3_mono_lemma RS lfp_Tarski RS ssubst) 1);
 by (rtac Un_upper2 1);
 val coinduct3_lemma = result();
 
-val prems = goal Gfp.thy
+val ainA::prems = goal Gfp.thy
     "[| a:A;  A <= f(lfp(%x.f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)";
-by (rtac (coinduct3_lemma RSN (2,coinduct)) 1);
-brs (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1;
-br (UnI2 RS UnI1) 1;
-by (REPEAT (resolve_tac prems 1));
+by (rtac coinduct 1);
+by (rtac (prems MRS coinduct3_lemma) 2);
+by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
+by (rtac (ainA RS UnI2 RS UnI1) 1);
 val coinduct3 = result();
 
 

--- a/src/CCL/Hered.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/Hered.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -13,7 +13,7 @@
 (*** Hereditary Termination ***)
 
 goalw Hered.thy [HTTgen_def]  "mono(%X.HTTgen(X))";
-br monoI 1;
+by (rtac monoI 1);
 by (fast_tac set_cs 1);
 val HTTgen_mono = result();
 
@@ -46,12 +46,12 @@
 val HTT_false = result();
 
 goal Hered.thy "<a,b> : HTT <->  a : HTT  & b : HTT";
-br (HTTXH RS iff_trans) 1;
+by (rtac (HTTXH RS iff_trans) 1);
 by (fast_tac term_cs 1);
 val HTT_pair = result();
 
 goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
-br (HTTXH RS iff_trans) 1;
+by (rtac (HTTXH RS iff_trans) 1);
 by (simp_tac term_ss 1);
 by (safe_tac term_cs);
 by (asm_simp_tac term_ss 1);
@@ -78,7 +78,7 @@
 (*** Coinduction for HTT ***)
 
 val prems = goal Hered.thy "[|  t : R;  R <= HTTgen(R) |] ==> t : HTT";
-br (HTT_def RS def_coinduct) 1;
+by (rtac (HTT_def RS def_coinduct) 1);
 by (REPEAT (ares_tac prems 1));
 val HTT_coinduct = result();
 
@@ -86,7 +86,7 @@
 
 val prems = goal Hered.thy 
     "[|  t : R;   R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT";
-br (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1;
+by (rtac (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1);
 by (REPEAT (ares_tac prems 1));
 val HTT_coinduct3 = result();
 val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3;
@@ -139,20 +139,20 @@
 goal Hered.thy "Nat <= HTT";
 by (simp_tac (term_ss addsimps [subsetXH]) 1);
 by (safe_tac set_cs);
-be Nat_ind 1;
+by (etac Nat_ind 1);
 by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD]))));
 val NatF = result();
 
 goal Hered.thy "Nat <= HTT";
 by (safe_tac set_cs);
-be HTT_coinduct3 1;
+by (etac HTT_coinduct3 1);
 by (fast_tac (set_cs addIs HTTgenIs 
                  addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1);
 val NatF = result();
 
 val [prem] = goal Hered.thy "A <= HTT ==> List(A) <= HTT";
 by (safe_tac set_cs);
-be HTT_coinduct3 1;
+by (etac HTT_coinduct3 1);
 by (fast_tac (set_cs addSIs HTTgenIs 
                  addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
                  addEs [XH_to_E ListXH]) 1);
@@ -160,7 +160,7 @@
 
 val [prem] = goal Hered.thy "A <= HTT ==> Lists(A) <= HTT";
 by (safe_tac set_cs);
-be HTT_coinduct3 1;
+by (etac HTT_coinduct3 1);
 by (fast_tac (set_cs addSIs HTTgenIs 
                  addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
                  addEs [XH_to_E ListsXH]) 1);
@@ -168,7 +168,7 @@
 
 val [prem] = goal Hered.thy "A <= HTT ==> ILists(A) <= HTT";
 by (safe_tac set_cs);
-be HTT_coinduct3 1;
+by (etac HTT_coinduct3 1);
 by (fast_tac (set_cs addSIs HTTgenIs 
                  addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
                  addEs [XH_to_E IListsXH]) 1);
@@ -181,7 +181,7 @@
 by (po_coinduct_tac "{p. EX a b.p=<a,b> & b : HTT & b [= a}" 1);
 by (fast_tac (ccl_cs addIs prems) 1);
 by (safe_tac ccl_cs);
-bd (poXH RS iffD1) 1;
+by (dtac (poXH RS iffD1) 1);
 by (safe_tac (set_cs addSEs [HTT_bot RS notE]));
 by (REPEAT_SOME (rtac (POgenXH RS iffD2) ORELSE' etac rev_mp));
 by (ALLGOALS (simp_tac (term_ss addsimps HTT_rews)));

--- a/src/CCL/Set.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/Set.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -117,7 +117,7 @@
  (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
 
 goal Set.thy "!!A B C. [| A<=B;  B<=C |] ==> A<=C";
-br subsetI 1;
+by (rtac subsetI 1);
 by (REPEAT (eresolve_tac [asm_rl, subsetD] 1));
 val subset_trans = result();
 
@@ -164,7 +164,7 @@
 val setup_induction = result();
 
 goal Set.thy "{x.x:A} = A";
-by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1  ORELSE eresolve_tac [CollectD] 1));
+by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1  ORELSE etac CollectD 1));
 val trivial_set = result();
 
 (*** Rules for binary union -- Un ***)
@@ -235,7 +235,7 @@
 (*** Empty sets ***)
 
 goalw Set.thy [empty_def] "{x.False} = {}";
-br refl 1;
+by (rtac refl 1);
 val empty_eq = result();
 
 val [prem] = goalw Set.thy [empty_def] "a : {} ==> P";
@@ -245,8 +245,8 @@
 val emptyE = make_elim emptyD;
 
 val [prem] = goal Set.thy "~ A={} ==> (EX x.x:A)";
-br (prem RS swap) 1;
-br equalityI 1;
+by (rtac (prem RS swap) 1);
+by (rtac equalityI 1);
 by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD])));
 val not_emptyD = result();
 

--- a/src/CCL/Term.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/Term.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -27,11 +27,11 @@
 val letB = result() RS mp;
 
 goalw Term.thy [let_def] "let x be bot in f(x) = bot";
-br caseBbot 1;
+by (rtac caseBbot 1);
 val letBabot = result();
 
 goalw Term.thy [let_def] "let x be t in bot = bot";
-brs ([caseBbot] RL [term_case]) 1;
+by (resolve_tac ([caseBbot] RL [term_case]) 1);
 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
 val letBbbot = result();
 
@@ -40,17 +40,17 @@
 val applyB = result();
 
 goalw Term.thy [apply_def] "bot ` a = bot";
-br caseBbot 1;
+by (rtac caseBbot 1);
 val applyBbot = result();
 
 goalw Term.thy [fix_def] "fix(f) = f(fix(f))";
-by (resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1);
+by (resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
 val fixB = result();
 
 goalw Term.thy [letrec_def]
       "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))";
 by (resolve_tac [fixB RS ssubst] 1 THEN 
-    resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1);
+    resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
 val letrecB = result();
 
 val rawBs = caseBs @ [applyB,applyBbot];

--- a/src/CCL/Trancl.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/Trancl.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -86,14 +86,14 @@
 
 (*Reflexivity of rtrancl*)
 goal Trancl.thy "<a,a> : r^*";
-br (rtrancl_unfold RS ssubst) 1;
+by (rtac (rtrancl_unfold RS ssubst) 1);
 by (fast_tac comp_cs 1);
 val rtrancl_refl = result();
 
 (*Closure under composition with r*)
 val prems = goal Trancl.thy
     "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*";
-br (rtrancl_unfold RS ssubst) 1;
+by (rtac (rtrancl_unfold RS ssubst) 1);
 by (fast_tac (comp_cs addIs prems) 1);
 val rtrancl_into_rtrancl = result();
 

--- a/src/CCL/Type.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/Type.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -67,7 +67,7 @@
                        (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
                        (ALLGOALS (asm_simp_tac term_ss)),
                        (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' 
-                                  eresolve_tac [bspec])),
+                                  etac bspec )),
                        (safe_tac (ccl_cs addSIs prems))]);
 end;
 
@@ -118,13 +118,13 @@
 
 val major::prems = goal Type.thy
     "mono(%X.A(X)) ==> mono(%X.[A(X)])";
-br (subsetI RS monoI) 1;
-bd (LiftXH RS iffD1) 1;
-be disjE 1;
-be (disjI1 RS (LiftXH RS iffD2)) 1;
-br (disjI2 RS (LiftXH RS iffD2)) 1;
-be (major RS monoD RS subsetD) 1;
-ba 1;
+by (rtac (subsetI RS monoI) 1);
+by (dtac (LiftXH RS iffD1) 1);
+by (etac disjE 1);
+by (etac (disjI1 RS (LiftXH RS iffD2)) 1);
+by (rtac (disjI2 RS (LiftXH RS iffD2)) 1);
+by (etac (major RS monoD RS subsetD) 1);
+by (assume_tac 1);
 val LiftM = result();
 
 val prems = goal Type.thy
@@ -261,8 +261,8 @@
 val [major,minor] = goal Type.thy
     "[| <a,b> : Sigma(A,B);  [| a:A;  b:B(a) |] ==> P   \
 \    |] ==> P";
-br (major RS (XH_to_E SgXH)) 1;
-br minor 1;
+by (rtac (major RS (XH_to_E SgXH)) 1);
+by (rtac minor 1);
 by (ALLGOALS (fast_tac term_cs));
 val SgE2 = result();
 
@@ -277,15 +277,15 @@
 (*** Infinite Data Types ***)
 
 val [mono] = goal Type.thy "mono(f) ==> lfp(f) <= gfp(f)";
-br (lfp_lowerbound RS subset_trans) 1;
-br (mono RS gfp_lemma3) 1;
-br subset_refl 1;
+by (rtac (lfp_lowerbound RS subset_trans) 1);
+by (rtac (mono RS gfp_lemma3) 1);
+by (rtac subset_refl 1);
 val lfp_subset_gfp = result();
 
 val prems = goal Type.thy
     "[| a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
 \    t(a) : gfp(B)";
-br coinduct 1;
+by (rtac coinduct 1);
 by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
 by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
 val gfpI = result();
@@ -302,7 +302,7 @@
 val prems = goal Type.thy 
     "letrec g x be zero$g(x) in g(bot) : Lists(Nat)";
 by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
-br (letrecB RS ssubst) 1;
-bw cons_def;
+by (rtac (letrecB RS ssubst) 1);
+by (rewtac cons_def);
 by (fast_tac type_cs 1);
 result();

--- a/src/CCL/Wfd.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/Wfd.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -26,7 +26,7 @@
     "[| !!x y.<x,y> : R ==> Q(x); \
 \       ALL x. (ALL y. <y,x> : R --> y : P) --> x : P; \
 \       !!x.Q(x) ==> x:P |] ==> a:P";
-br (p2 RS  spec  RS mp) 1;
+by (rtac (p2 RS  spec  RS mp) 1);
 by (fast_tac (set_cs addSIs [p1 RS p3]) 1);
 val wfd_strengthen_lemma = result();
 
@@ -36,7 +36,7 @@
 val wfd::prems = goal Wfd.thy "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P";
 by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
 by (fast_tac (FOL_cs addIs prems) 1);
-br (wfd RS  wfd_induct) 1;
+by (rtac (wfd RS  wfd_induct) 1);
 by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
 val wf_anti_sym = result();
 
@@ -53,11 +53,11 @@
 (*must retain the universal formula for later use!*)
 by (rtac allE 1 THEN assume_tac 1);
 by (etac mp 1);
-br (prem RS wfd_induct) 1;
+by (rtac (prem RS wfd_induct) 1);
 by (rtac (impI RS allI) 1);
 by (etac tranclE 1);
 by (fast_tac ccl_cs 1);
-be (spec RS mp RS spec RS mp) 1;
+by (etac (spec RS mp RS spec RS mp) 1);
 by (REPEAT (atac 1));
 val trancl_wf = result();
 
@@ -83,27 +83,27 @@
 \    !!a a' b b'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R;  \
 \    !!a b b'.[| <b,b'> : rb;  p = <<a,b>,<a,b'>> |] ==> R  |] ==> \
 \ R";
-br (major RS (lexXH RS iffD1) RS exE) 1;
+by (rtac (major RS (lexXH RS iffD1) RS exE) 1);
 by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
 by (ALLGOALS (fast_tac ccl_cs));
 val lexE = result();
 
 val [major,minor] = goal Wfd.thy
  "[| p : r**s;  !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P";
-br (major RS lexE) 1;
+by (rtac (major RS lexE) 1);
 by (ALLGOALS (fast_tac (set_cs addSEs [minor])));
 val lex_pair = result();
 
 val [wfa,wfb] = goal Wfd.thy
  "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)";
-bw Wfd_def;
+by (rewtac Wfd_def);
 by (safe_tac ccl_cs);
 by (wfd_strengthen_tac "%x.EX a b.x=<a,b>" 1);
 by (fast_tac (term_cs addSEs [lex_pair]) 1);
 by (subgoal_tac "ALL a b.<a,b>:P" 1);
 by (fast_tac ccl_cs 1);
-br (wfa RS wfd_induct RS allI) 1;
-br (wfb RS wfd_induct RS allI) 1;back();
+by (rtac (wfa RS wfd_induct RS allI) 1);
+by (rtac (wfb RS wfd_induct RS allI) 1);back();
 by (fast_tac (type_cs addSEs [lexE]) 1);
 val lex_wf = result();
 
@@ -121,40 +121,40 @@
 
 val major::prems = goal Wfd.thy
  "[| p : wmap(f,r);  !!a b.[| <f(a),f(b)> : r;  p=<a,b> |] ==> R |] ==> R";
-br (major RS (wmapXH RS iffD1) RS exE) 1;
+by (rtac (major RS (wmapXH RS iffD1) RS exE) 1);
 by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
 by (ALLGOALS (fast_tac ccl_cs));
 val wmapE = result();
 
 val [wf] = goal Wfd.thy
  "Wfd(r) ==> Wfd(wmap(f,r))";
-bw Wfd_def;
+by (rewtac Wfd_def);
 by (safe_tac ccl_cs);
 by (subgoal_tac "ALL b.ALL a.f(a)=b-->a:P" 1);
 by (fast_tac ccl_cs 1);
-br (wf RS wfd_induct RS allI) 1;
+by (rtac (wf RS wfd_induct RS allI) 1);
 by (safe_tac ccl_cs);
-be (spec RS mp) 1;
+by (etac (spec RS mp) 1);
 by (safe_tac (ccl_cs addSEs [wmapE]));
-be (spec RS mp RS spec RS mp) 1;
-ba 1;
-br refl 1;
+by (etac (spec RS mp RS spec RS mp) 1);
+by (assume_tac 1);
+by (rtac refl 1);
 val wmap_wf = result();
 
 (* Projections *)
 
 val prems = goal Wfd.thy "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
-br wmapI 1;
+by (rtac wmapI 1);
 by (simp_tac (term_ss addsimps prems) 1);
 val wfstI = result();
 
 val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
-br wmapI 1;
+by (rtac wmapI 1);
 by (simp_tac (term_ss addsimps prems) 1);
 val wsndI = result();
 
 val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)";
-br wmapI 1;
+by (rtac wmapI 1);
 by (simp_tac (term_ss addsimps prems) 1);
 val wthdI = result();
 
@@ -172,7 +172,7 @@
 val prems = goalw Wfd.thy [wf_def] "Wfd(wf(R))";
 by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1);
 by (ALLGOALS (asm_simp_tac CCL_ss));
-br Empty_wf 1;
+by (rtac Empty_wf 1);
 val wf_wf = result();
 
 goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
@@ -190,7 +190,7 @@
 by (safe_tac set_cs);
 by (wfd_strengthen_tac "%x.x:Nat" 1);
 by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
-be Nat_ind 1;
+by (etac Nat_ind 1);
 by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
 val NatPR_wf = result();
 
@@ -198,7 +198,7 @@
 by (safe_tac set_cs);
 by (wfd_strengthen_tac "%x.x:List(A)" 1);
 by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
-be List_ind 1;
+by (etac List_ind 1);
 by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH])));
 val ListPR_wf = result();
 

--- a/src/CCL/coinduction.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/coinduction.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -7,8 +7,8 @@
 *)
 
 val [mono,prem] = goal Lfp.thy "[| mono(f);  a : f(lfp(f)) |] ==> a : lfp(f)";
-br ((mono RS lfp_Tarski) RS ssubst) 1;
-br prem 1;
+by (rtac ((mono RS lfp_Tarski) RS ssubst) 1);
+by (rtac prem 1);
 val lfpI = result();
 
 val prems = goal CCL.thy "[| a=a';  a' : A |] ==> a : A";
@@ -41,7 +41,7 @@
 (** POgen **)
 
 goal Term.thy "<a,a> : PO";
-br (po_refl RS (XH_to_D PO_iff)) 1;
+by (rtac (po_refl RS (XH_to_D PO_iff)) 1);
 val PO_refl = result();
 
 val POgenIs = map (mk_genIs Term.thy data_defs POgenXH POgen_mono)
@@ -71,7 +71,7 @@
 (** EQgen **)
 
 goal Term.thy "<a,a> : EQ";
-br (refl RS (EQ_iff RS iffD1)) 1;
+by (rtac (refl RS (EQ_iff RS iffD1)) 1);
 val EQ_refl = result();
 
 val EQgenIs = map (mk_genIs Term.thy data_defs EQgenXH EQgen_mono)

--- a/src/CCL/eval.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/eval.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -22,16 +22,16 @@
 
 val major::prems = goalw thy [let_def]
    "[| t ---> a;  f(a) ---> c |] ==> let x be t in f(x) ---> c";
-br (major RS canonical) 1;
+by (rtac (major RS canonical) 1);
 by (REPEAT (DEPTH_SOLVE_1 (resolve_tac ([major]@prems@(!EVal_rls)) 1 ORELSE
-                           eresolve_tac [substitute] 1)));
+                           etac substitute 1)));
 val letV = result();
 
 val prems = goalw thy [fix_def]
    "f(fix(f)) ---> c ==> fix(f) ---> c";
-br applyV 1;
-br lamV 1;
-brs prems 1;
+by (rtac applyV 1);
+by (rtac lamV 1);
+by (resolve_tac prems 1);
 val fixV = result();
 
 val prems = goalw thy [letrec_def]

--- a/src/CCL/genrec.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/genrec.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -12,18 +12,18 @@
 \       !!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==>\
 \               h(p,g) : D(p) |] ==> \
 \    letrec g x be h(x,g) in g(a) : D(a)";
-br (major RS rev_mp) 1;
-br (wf_wf RS wfd_induct) 1;
-br (letrecB RS ssubst) 1;
-br impI 1;
-bes prems 1;
-br ballI 1;
-be (spec RS mp RS mp) 1;
+by (rtac (major RS rev_mp) 1);
+by (rtac (wf_wf RS wfd_induct) 1);
+by (rtac (letrecB RS ssubst) 1);
+by (rtac impI 1);
+by (eresolve_tac prems 1);
+by (rtac ballI 1);
+by (etac (spec RS mp RS mp) 1);
 by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1));
 val letrecT = result();
 
 goalw Wfd.thy [SPLIT_def] "SPLIT(<a,b>,B) = B(a,b)";
-br set_ext 1;
+by (rtac set_ext 1);
 by (fast_tac ccl_cs 1);
 val SPLITB = result();
 
@@ -33,11 +33,11 @@
 \             ALL x:A.ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
 \               h(p,q,g) : D(p,q) |] ==> \
 \    letrec g x y be h(x,y,g) in g(a,b) : D(a,b)";
-br (SPLITB RS subst) 1;
+by (rtac (SPLITB RS subst) 1);
 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1));
-br (SPLITB RS ssubst) 1;
+by (rtac (SPLITB RS ssubst) 1);
 by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1));
-br (SPLITB RS subst) 1;
+by (rtac (SPLITB RS subst) 1);
 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
             eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
 val letrec2T = result();
@@ -53,11 +53,11 @@
 \                                                       g(x,y,z) : D(x,y,z) |] ==>\
 \               h(p,q,r,g) : D(p,q,r) |] ==> \
 \    letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)";
-br (lemma RS subst) 1;
+by (rtac (lemma RS subst) 1);
 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1));
 by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
 by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1));
-br (lemma RS subst) 1;
+by (rtac (lemma RS subst) 1);
 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
             eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
 val letrec3T = result();
@@ -99,9 +99,9 @@
 \       ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A;  \
 \       ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R) |] ==> \
 \   P";
-brs (prems RL prems) 1;
-brs (prems RL [sym]) 1;
-br rcallT 1;
+by (resolve_tac (prems RL prems) 1);
+by (resolve_tac (prems RL [sym]) 1);
+by (rtac rcallT 1);
 by (REPEAT (ares_tac prems 1));
 val hyprcallT = result();
 
@@ -109,9 +109,9 @@
     "[| g(a) = b; ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);\
 \       [| b=g(a);  g(a) : D(a) |] ==> P; a:A;  <a,p>:wf(R) |] ==> \
 \   P";
-brs (prems) 1;
-brs (prems RL [sym]) 1;
-br rcallT 1;
+by (resolve_tac (prems) 1);
+by (resolve_tac (prems RL [sym]) 1);
+by (rtac rcallT 1);
 by (REPEAT (ares_tac prems 1));
 val hyprcallT = result();
 
@@ -120,9 +120,9 @@
 \       [| c=g(a,b);  g(a,b) : D(a,b) |] ==> P; \
 \       a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==> \
 \   P";
-brs (prems) 1;
-brs (prems RL [sym]) 1;
-br rcall2T 1;
+by (resolve_tac (prems) 1);
+by (resolve_tac (prems RL [sym]) 1);
+by (rtac rcall2T 1);
 by (REPEAT (ares_tac prems 1));
 val hyprcall2T = result();
 
@@ -132,9 +132,9 @@
 \   [| d=g(a,b,c);  g(a,b,c) : D(a,b,c) |] ==> P; \
 \   a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
 \   P";
-brs (prems) 1;
-brs (prems RL [sym]) 1;
-br rcall3T 1;
+by (resolve_tac (prems) 1);
+by (resolve_tac (prems RL [sym]) 1);
+by (rtac rcall3T 1);
 by (REPEAT (ares_tac prems 1));
 val hyprcall3T = result();
 

--- a/src/CCL/typecheck.ML	Wed Oct 12 16:38:58 1994 +0100
+++ b/src/CCL/typecheck.ML	Wed Oct 19 09:23:56 1994 +0100
@@ -13,7 +13,7 @@
 val Subtype_canTs = 
        let fun tac prems = cut_facts_tac prems 1 THEN
                 REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE
-                        eresolve_tac [SubtypeE] 1)
+                        etac SubtypeE 1)
            fun solve s = prove_goal Type.thy s (fn prems => [tac prems])
        in map solve
            ["P(one) ==> one : {x:Unit.P(x)}",
@@ -31,7 +31,7 @@
 val Subtype_canTs = 
        let fun tac prems = cut_facts_tac prems 1 THEN
                 REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE
-                        eresolve_tac [SubtypeE] 1)
+                        etac SubtypeE 1)
            fun solve s = prove_goal Type.thy s (fn prems => [tac prems])
        in map solve
            ["a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}",
@@ -44,8 +44,8 @@
 val prems = goal Type.thy
      "[| f(t):B;  ~t=bot  |] ==> let x be t in f(x) : B";
 by (cut_facts_tac prems 1);
-be (letB RS ssubst) 1;
-ba 1;
+by (etac (letB RS ssubst) 1);
+by (assume_tac 1);
 val letT = result();
 
 val prems = goal Type.thy