src/HOL/Nitpick_Examples/Manual_Nits.thy

 (* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
    we cannot rely on its presence, we expediently provide our own
    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"
 unfolding llist_def by auto
 

 
 declaration {*
 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]
 oops