--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Jan 03 23:03:49 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Jan 03 23:09:27 2012 +0100
@@ -197,6 +197,7 @@
axiomatization. The examples also work unchanged with Lochbihler's
"Coinductive_List" theory. *)
+(* BEGIN LAZY LIST SETUP *)
definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
@@ -219,6 +220,7 @@
Nitpick_HOL.register_codatatype @{typ "'a llist"} ""
(map dest_Const [@{term LNil}, @{term LCons}])
*}
+(* END LAZY LIST SETUP *)
lemma "xs \<noteq> LCons a xs"
nitpick [expect = genuine]