Removed some case_names and consumes attributes that are now no longer
authorberghofe
Tue Nov 13 11:02:55 2007 +0100 (2007-11-13)
changeset 254259191942c4ead
parent 25424 170f4cc34697
child 25426 7ab693b8ee87
Removed some case_names and consumes attributes that are now no longer
needed due to changes in the to_pred and to_set attributes.
src/HOL/Transitive_Closure.thy
src/HOL/Wellfounded_Recursion.thy
     1.1 --- a/src/HOL/Transitive_Closure.thy	Tue Nov 13 11:00:29 2007 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Nov 13 11:02:55 2007 +0100
     1.3 @@ -97,7 +97,7 @@
     1.4    thus ?thesis by iprover
     1.5  qed
     1.6  
     1.7 -lemmas rtrancl_induct [consumes 1, induct set: rtrancl] = rtranclp_induct [to_set]
     1.8 +lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set]
     1.9  
    1.10  lemmas rtranclp_induct2 =
    1.11    rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule,
    1.12 @@ -241,7 +241,7 @@
    1.13      by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+
    1.14  qed
    1.15  
    1.16 -lemmas converse_rtrancl_induct[consumes 1] = converse_rtranclp_induct [to_set]
    1.17 +lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set]
    1.18  
    1.19  lemmas converse_rtranclp_induct2 =
    1.20    converse_rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule,
    1.21 @@ -324,7 +324,7 @@
    1.22    thus ?thesis by iprover
    1.23  qed
    1.24  
    1.25 -lemmas trancl_induct [consumes 1, induct set: trancl] = tranclp_induct [to_set]
    1.26 +lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set]
    1.27  
    1.28  lemmas tranclp_induct2 =
    1.29    tranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule,
     2.1 --- a/src/HOL/Wellfounded_Recursion.thy	Tue Nov 13 11:00:29 2007 +0100
     2.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Tue Nov 13 11:02:55 2007 +0100
     2.3 @@ -71,8 +71,7 @@
     2.4  
     2.5  lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
     2.6  
     2.7 -lemmas wfP_induct_rule =
     2.8 -  wf_induct_rule [to_pred, consumes 1, case_names less, induct set: wfP]
     2.9 +lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
    2.10  
    2.11  lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r"
    2.12  by (erule_tac a=a in wf_induct, blast)