# HG changeset patch
# User oheimb
# Date 991320774 -7200
# Node ID fcb507c945c3832faf0d10daf37015269c54e76c
# Parent  e08a0855af67cc33f412fdd2fa3b3c4e2893984c
added Library/Nat_Infinity.thy and Library/Continuity.thy

diff -r e08a0855af67 -r fcb507c945c3 src/HOL/IsaMakefile
--- 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
diff -r e08a0855af67 -r fcb507c945c3 src/HOL/Library/Library.thy
--- 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:
diff -r e08a0855af67 -r fcb507c945c3 src/HOL/Library/ROOT.ML
--- 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";
diff -r e08a0855af67 -r fcb507c945c3 src/HOL/Library/document/root.bib
--- 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
diff -r e08a0855af67 -r fcb507c945c3 src/HOL/Library/document/root.tex
--- 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}