--- a/src/HOL/IsaMakefile Thu May 31 16:52:47 2001 +0200
+++ b/src/HOL/IsaMakefile Thu May 31 16:52:54 2001 +0200
@@ -182,7 +182,8 @@
$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
Library/Permutation.thy Library/Quotient.thy Library/Ring_and_Field.thy \
- Library/Ring_and_Field_Example.thy Library/README.html \
+ Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
+ Library/README.html Library/Continuity.thy \
Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \
Library/While_Combinator.thy
@$(ISATOOL) usedir $(OUT)/HOL Library
--- a/src/HOL/Library/Library.thy Thu May 31 16:52:47 2001 +0200
+++ b/src/HOL/Library/Library.thy Thu May 31 16:52:54 2001 +0200
@@ -2,10 +2,12 @@
theory Library =
Quotient +
Ring_and_Field + Ring_and_Field_Example +
+ Nat_Infinity +
Rational_Numbers +
List_Prefix +
Nested_Environment +
Accessible_Part +
+ Continuity +
Multiset +
Permutation +
While_Combinator:
--- a/src/HOL/Library/ROOT.ML Thu May 31 16:52:47 2001 +0200
+++ b/src/HOL/Library/ROOT.ML Thu May 31 16:52:54 2001 +0200
@@ -1,2 +1,1 @@
-
use_thy "Library";
--- a/src/HOL/Library/document/root.bib Thu May 31 16:52:47 2001 +0200
+++ b/src/HOL/Library/document/root.bib Thu May 31 16:52:54 2001 +0200
@@ -1,4 +1,3 @@
-
@InProceedings{paulin-tlca,
author = {Christine Paulin-Mohring},
title = {Inductive Definitions in the System {Coq}: Rules and
--- a/src/HOL/Library/document/root.tex Thu May 31 16:52:47 2001 +0200
+++ b/src/HOL/Library/document/root.tex Thu May 31 16:52:54 2001 +0200
@@ -15,6 +15,7 @@
\author{
Gertrud Bauer \\
Tobias Nipkow \\
+ David von Oheimb\\
Lawrence C Paulson \\
Thomas M Rasmussen \\
Markus Wenzel}