src/CCL/coinduction.ML

 
 Lemmas and tactics for using the rule coinduct3 on [= and =.
 *)
 
 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";
 by (simp_tac (term_ss addsimps prems) 1);
 val ssubst_single = result();

                              @ prems)) 1)]);
 
 (** 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)
       ["<true,true> : POgen(R)",
        "<false,false> : POgen(R)",

                    (POgenIs RL [POgen_mono RS ci3_AgenI]) @ [POgen_mono RS ci3_RI]) i));
 
 (** 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)
 ["<true,true> : EQgen(R)",
  "<false,false> : EQgen(R)",