equal
deleted
inserted
replaced
713 |
713 |
714 |
714 |
715 |
715 |
716 (** Termination rule **) |
716 (** Termination rule **) |
717 |
717 |
718 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} |
718 val wf_induct_rule = @{thm Wellfounded.wfp_induct_rule} |
719 val wf_in_rel = @{thm Fun_Def.wf_in_rel} |
719 val wf_in_rel = @{thm Fun_Def.wf_in_rel} |
720 val in_rel_def = @{thm Fun_Def.in_rel_def} |
720 val in_rel_def = @{thm Fun_Def.in_rel_def} |
721 |
721 |
722 fun mk_nest_term_case ctxt globals R' ihyp clause = |
722 fun mk_nest_term_case ctxt globals R' ihyp clause = |
723 let |
723 let |