# HG changeset patch
# User blanchet
# Date 1325628567 -3600
# Node ID 73e2c70980dfbb75866cfdac02822f5e782f86f3
# Parent  9abb756352a6cec3d985e8726af8f204ae53fd82
tuning

diff -r 9abb756352a6 -r 73e2c70980df src/HOL/Nitpick_Examples/Manual_Nits.thy
--- 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]