Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added HOL/Library/Coinductive_List.thy;
authorwenzelm
Tue, 13 Dec 2005 19:32:04 +0100
changeset 18397 2d94eb7ff17f
parent 18396 b3e7da94b51f
child 18398 5d63a8b35688
added HOL/Library/Coinductive_List.thy;
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/Library/Library.thy file | annotate | diff | comparison | revisions 
--- 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
 
 
--- 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
 (*>*)
isabelle