# HG changeset patch
# User wenzelm
# Date 1134498724 -3600
# Node ID 2d94eb7ff17f796e671efd9368c2d561767c1a5f
# Parent  b3e7da94b51fd5288df0c363dc300b0708d92b1f
added HOL/Library/Coinductive_List.thy;

diff -r b3e7da94b51f -r 2d94eb7ff17f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Dec 13 18:11:21 2005 +0100
+++ b/src/HOL/IsaMakefile	Tue Dec 13 19:32:04 2005 +0100
@@ -191,7 +191,8 @@
   Library/Library/ROOT.ML Library/Library/document/root.tex \
   Library/Library/document/root.bib Library/While_Combinator.thy \
   Library/Product_ord.thy Library/Char_ord.thy \
-  Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML
+  Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
+  Library/Coinductive_List.thy
 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
 
 
diff -r b3e7da94b51f -r 2d94eb7ff17f src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Dec 13 18:11:21 2005 +0100
+++ b/src/HOL/Library/Library.thy	Tue Dec 13 19:32:04 2005 +0100
@@ -20,6 +20,7 @@
   Zorn
   Char_ord
   Commutative_Ring
+  Coinductive_List
 begin
 end
 (*>*)