src/ZF/Induct/Comb.thy

 text {*
   \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}.
 *}
 
 lemma contract_imp_parcontract: "p-1->q ==> p=1=>q"
-  by (erule contract.induct) auto
+  by (induct set: contract) auto
 
 lemma reduce_imp_parreduce: "p--->q ==> p===>q"
   apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
   apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
   apply (erule rtrancl_induct)

   apply (blast intro: contract_imp_parcontract r_into_trancl
     trans_trancl [THEN transD])
   done
 
 lemma parcontract_imp_reduce: "p=1=>q ==> p--->q"
-  apply (erule parcontract.induct)
+  apply (induct set: parcontract)
      apply (blast intro: reduction_rls)
     apply (blast intro: reduction_rls)
    apply (blast intro: reduction_rls)
   apply (blast intro: trans_rtrancl [THEN transD]
     Ap_reduce1 Ap_reduce2 parcontract_combD1 parcontract_combD2)