use "primcorec" in example
authorblanchet
Tue, 24 Sep 2013 16:59:14 +0200
changeset 53827 62c2f66ff9b2
parent 53826 92a8ae172242
child 53828 408c9a3617e3
use "primcorec" in example
src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Sep 24 16:55:29 2013 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Sep 24 16:59:14 2013 +0200
@@ -195,8 +195,8 @@
 
 codatatype 'a llist = LNil | LCons 'a "'a llist"
 
-primcorecursive iterates where
-"iterates f a = LCons a (iterates f (f a))" .
+primcorec iterates where
+"iterates f a = LCons a (iterates f (f a))"
 
 lemma "xs \<noteq> LCons a xs"
 nitpick [expect = genuine]