# 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}