src/HOL/Wellfounded.thy
changeset 61337 4645502c3c64
parent 60758 d8d85a8172b5
child 61424 c3658c18b7bc
     1.1 --- a/src/HOL/Wellfounded.thy	Tue Oct 06 13:31:44 2015 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Oct 06 15:14:28 2015 +0200
     1.3 @@ -558,7 +558,7 @@
     1.4    apply fast
     1.5    done
     1.6  
     1.7 -theorems accp_induct_rule = accp_induct [rule_format, induct set: accp]
     1.8 +lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp]
     1.9  
    1.10  theorem accp_downward: "accp r b ==> r a b ==> accp r a"
    1.11    apply (erule accp.cases)