author | blanchet |
Tue, 24 Sep 2013 16:59:14 +0200 | |
changeset 53827 | 62c2f66ff9b2 |
parent 53826 | 92a8ae172242 |
child 53828 | 408c9a3617e3 |
--- 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]