diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -13,6 +13,7 @@
 
 definition
   "NIL = Datatype.In0 (Datatype.Numb 0)"
+definition
   "CONS M N = Datatype.In1 (Datatype.Scons M N)"
 
 lemma CONS_not_NIL [iff]: "CONS M N \<noteq> NIL"
@@ -146,6 +147,7 @@
 
 definition
   "LNil = Abs_llist NIL"
+definition
   "LCons x xs = Abs_llist (CONS (Datatype.Leaf x) (Rep_llist xs))"
 
 lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil"
@@ -573,6 +575,7 @@
 
 definition
   "Lmap f M = LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))"
+definition
   "lmap f l = llist_corec l
     (\<lambda>z.
       case z of LNil \<Rightarrow> None
@@ -671,6 +674,7 @@
     (split (List_case
         (List_case None (\<lambda>N1 N2. Some (N1, (NIL, N2))))
         (\<lambda>M1 M2 N. Some (M1, (M2, N)))))"
+definition
   "lappend l n = llist_corec (l, n)
     (split (llist_case
         (llist_case None (\<lambda>n1 n2. Some (n1, (LNil, n2))))
@@ -746,7 +750,7 @@
 text {* @{text llist_fun_equalityI} cannot be used here! *}
 
 definition
-  iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
+  iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
   "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
 
 lemma iterates: "iterates f x = LCons x (iterates f (f x))"