src/ZF/indrule.ML
changeset 543 e961b2092869
parent 516 1957113f0d7d
child 590 800603278425
     1.1 --- a/src/ZF/indrule.ML	Thu Aug 18 12:56:57 1994 +0200
     1.2 +++ b/src/ZF/indrule.ML	Thu Aug 18 17:41:40 1994 +0200
     1.3 @@ -69,9 +69,10 @@
     1.4  val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;
     1.5  
     1.6  val quant_induct = 
     1.7 -    prove_term sign part_rec_defs 
     1.8 -      (list_implies (ind_prems, mk_tprop (mk_all_imp(big_rec_tm,pred))),
     1.9 -       fn prems =>
    1.10 +    prove_goalw_cterm part_rec_defs 
    1.11 +      (cterm_of sign (list_implies (ind_prems, 
    1.12 +				    mk_tprop (mk_all_imp(big_rec_tm,pred)))))
    1.13 +      (fn prems =>
    1.14         [rtac (impI RS allI) 1,
    1.15  	etac raw_induct 1,
    1.16  	REPEAT (FIRSTGOAL (eresolve_tac [CollectE,exE,conjE,disjE,ssubst])),
    1.17 @@ -118,9 +119,9 @@
    1.18  and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);
    1.19  
    1.20  val lemma = (*makes the link between the two induction rules*)
    1.21 -    prove_term sign part_rec_defs 
    1.22 -	  (mk_implies (induct_concl,mutual_induct_concl), 
    1.23 -	   fn prems =>
    1.24 +    prove_goalw_cterm part_rec_defs 
    1.25 +	  (cterm_of sign (mk_implies (induct_concl,mutual_induct_concl)))
    1.26 +	  (fn prems =>
    1.27  	   [cut_facts_tac prems 1,
    1.28  	    REPEAT (eresolve_tac [asm_rl,conjE,PartE,mp] 1
    1.29  	     ORELSE resolve_tac [allI,impI,conjI,Part_eqI] 1
    1.30 @@ -145,10 +146,11 @@
    1.31  	i  THEN mutual_ind_tac prems (i-1);
    1.32  
    1.33  val mutual_induct_fsplit = 
    1.34 -    prove_term sign []
    1.35 -	  (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
    1.36 -			 mutual_induct_concl),
    1.37 -	   fn prems =>
    1.38 +    prove_goalw_cterm []
    1.39 +	  (cterm_of sign
    1.40 +	   (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
    1.41 +			  mutual_induct_concl)))
    1.42 +	  (fn prems =>
    1.43  	   [rtac (quant_induct RS lemma) 1,
    1.44  	    mutual_ind_tac (rev prems) (length prems)]);
    1.45