added HOL/Library/Coinductive_List.thy;
authorwenzelm
Tue Dec 13 19:32:04 2005 +0100 (2005-12-13)
changeset 183972d94eb7ff17f
parent 18396 b3e7da94b51f
child 18398 5d63a8b35688
added HOL/Library/Coinductive_List.thy;
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Dec 13 18:11:21 2005 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Dec 13 19:32:04 2005 +0100
     1.3 @@ -191,7 +191,8 @@
     1.4    Library/Library/ROOT.ML Library/Library/document/root.tex \
     1.5    Library/Library/document/root.bib Library/While_Combinator.thy \
     1.6    Library/Product_ord.thy Library/Char_ord.thy \
     1.7 -  Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML
     1.8 +  Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
     1.9 +  Library/Coinductive_List.thy
    1.10  	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
    1.11  
    1.12  
     2.1 --- a/src/HOL/Library/Library.thy	Tue Dec 13 18:11:21 2005 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Tue Dec 13 19:32:04 2005 +0100
     2.3 @@ -20,6 +20,7 @@
     2.4    Zorn
     2.5    Char_ord
     2.6    Commutative_Ring
     2.7 +  Coinductive_List
     2.8  begin
     2.9  end
    2.10  (*>*)