added Library/Nat_Infinity.thy and Library/Continuity.thy
authoroheimb
Thu May 31 16:52:54 2001 +0200 (2001-05-31)
changeset 11349fcb507c945c3
parent 11348 e08a0855af67
child 11350 4c55b020d6ee
added Library/Nat_Infinity.thy and Library/Continuity.thy
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/ROOT.ML
src/HOL/Library/document/root.bib
src/HOL/Library/document/root.tex
     1.1 --- a/src/HOL/IsaMakefile	Thu May 31 16:52:47 2001 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu May 31 16:52:54 2001 +0200
     1.3 @@ -182,7 +182,8 @@
     1.4  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
     1.5    Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
     1.6    Library/Permutation.thy Library/Quotient.thy Library/Ring_and_Field.thy \
     1.7 -  Library/Ring_and_Field_Example.thy Library/README.html \
     1.8 +  Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
     1.9 +  Library/README.html Library/Continuity.thy \
    1.10    Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \
    1.11    Library/While_Combinator.thy
    1.12  	@$(ISATOOL) usedir $(OUT)/HOL Library
     2.1 --- a/src/HOL/Library/Library.thy	Thu May 31 16:52:47 2001 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Thu May 31 16:52:54 2001 +0200
     2.3 @@ -2,10 +2,12 @@
     2.4  theory Library =
     2.5    Quotient +
     2.6    Ring_and_Field + Ring_and_Field_Example +
     2.7 +  Nat_Infinity +
     2.8    Rational_Numbers +
     2.9    List_Prefix +
    2.10    Nested_Environment +
    2.11    Accessible_Part +
    2.12 +  Continuity +
    2.13    Multiset +
    2.14    Permutation +
    2.15    While_Combinator:
     3.1 --- a/src/HOL/Library/ROOT.ML	Thu May 31 16:52:47 2001 +0200
     3.2 +++ b/src/HOL/Library/ROOT.ML	Thu May 31 16:52:54 2001 +0200
     3.3 @@ -1,2 +1,1 @@
     3.4 -
     3.5  use_thy "Library";
     4.1 --- a/src/HOL/Library/document/root.bib	Thu May 31 16:52:47 2001 +0200
     4.2 +++ b/src/HOL/Library/document/root.bib	Thu May 31 16:52:54 2001 +0200
     4.3 @@ -1,4 +1,3 @@
     4.4 -
     4.5  @InProceedings{paulin-tlca,
     4.6    author	= {Christine Paulin-Mohring},
     4.7    title		= {Inductive Definitions in the System {Coq}: Rules and
     5.1 --- a/src/HOL/Library/document/root.tex	Thu May 31 16:52:47 2001 +0200
     5.2 +++ b/src/HOL/Library/document/root.tex	Thu May 31 16:52:54 2001 +0200
     5.3 @@ -15,6 +15,7 @@
     5.4  \author{
     5.5    Gertrud Bauer \\
     5.6    Tobias Nipkow \\
     5.7 +  David von Oheimb\\
     5.8    Lawrence C Paulson \\
     5.9    Thomas M Rasmussen \\
    5.10    Markus Wenzel}