src/HOL/Wellfounded_Recursion.thy
changeset 25425 9191942c4ead
parent 25207 d58c14280367
child 26044 32889481ec4c
     1.1 --- a/src/HOL/Wellfounded_Recursion.thy	Tue Nov 13 11:00:29 2007 +0100
     1.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Tue Nov 13 11:02:55 2007 +0100
     1.3 @@ -71,8 +71,7 @@
     1.4  
     1.5  lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
     1.6  
     1.7 -lemmas wfP_induct_rule =
     1.8 -  wf_induct_rule [to_pred, consumes 1, case_names less, induct set: wfP]
     1.9 +lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
    1.10  
    1.11  lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r"
    1.12  by (erule_tac a=a in wf_induct, blast)