Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Wellfounded.thy
changeset 61337 4645502c3c64
parent 60758 d8d85a8172b5
child 61424 c3658c18b7bc 
--- a/src/HOL/Wellfounded.thy	Tue Oct 06 13:31:44 2015 +0200
+++ b/src/HOL/Wellfounded.thy	Tue Oct 06 15:14:28 2015 +0200
@@ -558,7 +558,7 @@
   apply fast
   done
 
-theorems accp_induct_rule = accp_induct [rule_format, induct set: accp]
+lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp]
 
 theorem accp_downward: "accp r b ==> r a b ==> accp r a"
   apply (erule accp.cases)
isabelle