src/CCL/CCL.ML

 val caseBs = [caseBtrue,caseBfalse,caseBpair,caseBlam,caseBbot];
 
 (*** 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 ***)
 
 val prems = goal CCL.thy

                     addSDs (XH_to_Ds ccl_injs);
 
 (****** 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)";
 by (fast_tac ccl_cs 1);
 val XHlemma2 = result() RS mp;
 
 (*** 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));
 by (ALLGOALS (fast_tac set_cs));
 val POgen_mono = result();
 
 goalw CCL.thy [POgen_def,SIM_def]
   "<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
   "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
 \                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
 \                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.f(x) [= f'(x)))";
 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);
 by (fast_tac ccl_cs 1);
 val po_lam = result();

 val ccl_porews = [po_bot,po_pair,po_lam];
 
 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
     "[| f [= f';  a [= a' |] ==> f ` a [= f' ` a'";
 by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1));
 val apply_pocong = result();
 
 
 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();
 
 fun mk_thm s = prove_goal CCL.thy s (fn _ => 
                           [rtac notI 1,dtac case_pocong 1,etac rev_mp 5,

             "~ false [= lam x.f(x)","~ lam x.f(x) [= false"];
 
 (* 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();
 
 fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i;
 
 (*************** 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));
 by (ALLGOALS (fast_tac set_cs));
 val EQgen_mono = result();

 goalw CCL.thy [EQgen_def,SIM_def]
   "<t,t'> : EQgen(R) <-> (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'> : 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
   "t=t' <-> (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' & b=b') | \
 \                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.f(x)=f'(x)))";
 by (subgoal_tac
   "<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();
 
 fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i;
 fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i;