eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
--- a/src/HOL/IsaMakefile Tue May 25 20:28:16 2010 +0200
+++ b/src/HOL/IsaMakefile Tue May 25 21:49:44 2010 +0200
@@ -396,46 +396,47 @@
HOL-Library: HOL $(LOG)/HOL-Library.gz
-$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy \
- Library/Abstract_Rat.thy Library/BigO.thy Library/ContNotDenum.thy \
- Library/Efficient_Nat.thy Library/Sum_Of_Squares.thy \
- Library/Dlist.thy Library/Sum_Of_Squares/sos_wrapper.ML \
- Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy \
- Library/Glbs.thy Library/Executable_Set.thy \
- Library/Infinite_Set.thy Library/FuncSet.thy \
- Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy \
- Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy \
- Library/Inner_Product.thy Library/Kleene_Algebra.thy \
- Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \
- Library/Library.thy Library/List_Prefix.thy Library/More_Set.thy \
- Library/More_List.thy Library/Multiset.thy Library/Permutation.thy \
- Library/Quotient_Type.thy Library/Quicksort.thy \
- Library/Nat_Infinity.thy Library/README.html Library/State_Monad.thy \
- Library/Continuity.thy Library/Order_Relation.thy \
- Library/Nested_Environment.thy Library/Ramsey.thy Library/Zorn.thy \
- Library/Library/ROOT.ML Library/Library/document/root.tex \
- Library/Library/document/root.bib \
- Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
- Library/Product_ord.thy Library/Char_nat.thy \
- Library/Sublist_Order.thy Library/List_lexord.thy \
- Library/AssocList.thy Library/Formal_Power_Series.thy \
- Library/Binomial.thy Library/Eval_Witness.thy Library/Code_Char.thy \
- Library/Code_Char_chr.thy Library/Code_Integer.thy \
- Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy \
- Library/Boolean_Algebra.thy Library/Countable.thy \
- Library/Diagonalize.thy Library/RBT.thy Library/RBT_Impl.thy \
- Library/Univ_Poly.thy \
- Library/Poly_Deriv.thy Library/Polynomial.thy Library/Preorder.thy \
- Library/Product_plus.thy Library/Product_Vector.thy \
- Library/Enum.thy Library/Float.thy Library/Quotient_List.thy \
- Library/Quotient_Option.thy Library/Quotient_Product.thy \
- Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \
- Library/Nat_Bijection.thy $(SRC)/Tools/float.ML \
- $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML \
- Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy \
- Library/OptionalSugar.thy Library/Convex.thy \
- Library/Predicate_Compile_Quickcheck.thy Library/SML_Quickcheck.thy
- @cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
+$(LOG)/HOL-Library.gz: $(OUT)/HOL $(SRC)/HOL/Tools/float_arith.ML \
+ $(SRC)/Tools/float.ML Library/Abstract_Rat.thy Library/AssocList.thy \
+ Library/BigO.thy Library/Binomial.thy Library/Bit.thy \
+ Library/Boolean_Algebra.thy Library/Char_nat.thy \
+ Library/Code_Char.thy Library/Code_Char_chr.thy \
+ Library/Code_Integer.thy Library/ContNotDenum.thy \
+ Library/Continuity.thy Library/Convex.thy Library/Countable.thy \
+ Library/Diagonalize.thy Library/Dlist.thy Library/Efficient_Nat.thy \
+ Library/Enum.thy Library/Eval_Witness.thy Library/Executable_Set.thy \
+ Library/Float.thy Library/Formal_Power_Series.thy \
+ Library/Fraction_Field.thy Library/FrechetDeriv.thy Library/Fset.thy \
+ Library/FuncSet.thy Library/Fundamental_Theorem_Algebra.thy \
+ Library/Glbs.thy Library/Infinite_Set.thy Library/Inner_Product.thy \
+ Library/HOL_Library_ROOT.ML Library/Kleene_Algebra.thy \
+ Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \
+ Library/Lattice_Syntax.thy Library/Library.thy \
+ Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
+ Library/More_List.thy Library/More_Set.thy Library/Multiset.thy \
+ Library/Nat_Bijection.thy Library/Nat_Infinity.thy \
+ Library/Nested_Environment.thy Library/Numeral_Type.thy \
+ Library/OptionalSugar.thy Library/Order_Relation.thy \
+ Library/Permutation.thy Library/Permutations.thy \
+ Library/Poly_Deriv.thy Library/Polynomial.thy \
+ Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy \
+ Library/Product_Vector.thy Library/Product_ord.thy \
+ Library/Product_plus.thy Library/Quicksort.thy \
+ Library/Quotient_List.thy Library/Quotient_Option.thy \
+ Library/Quotient_Product.thy Library/Quotient_Sum.thy \
+ Library/Quotient_Syntax.thy Library/Quotient_Type.thy \
+ Library/RBT.thy Library/RBT_Impl.thy Library/README.html \
+ Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy \
+ Library/SML_Quickcheck.thy Library/SetsAndFunctions.thy \
+ Library/Sublist_Order.thy Library/Sum_Of_Squares.thy \
+ Library/Sum_Of_Squares/sos_wrapper.ML \
+ Library/Sum_Of_Squares/sum_of_squares.ML \
+ Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \
+ Library/While_Combinator.thy Library/Zorn.thy \
+ Library/document/root.bib Library/document/root.tex \
+ Library/positivstellensatz.ML Library/reflection.ML \
+ Library/reify_data.ML
+ @$(ISABELLE_TOOL) usedir -f HOL_Library_ROOT.ML $(OUT)/HOL Library
## HOL-Hahn_Banach
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/HOL_Library_ROOT.ML Tue May 25 21:49:44 2010 +0200
@@ -0,0 +1,1 @@
+use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"];
--- a/src/HOL/Library/Library/ROOT.ML Tue May 25 20:28:16 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"];
--- a/src/HOL/Library/Library/document/root.bib Tue May 25 20:28:16 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-
-@Unpublished{Abrial-Laffitte,
- author = {Abrial and Laffitte},
- title = {Towards the Mechanization of the Proofs of
- Some Classical Theorems of Set Theory},
- note = {Unpublished}
-}
-
-@InProceedings{Avigad-Donnelly,
- author = {Jeremy Avigad and Kevin Donnelly},
- title = {Formalizing {O} notation in {Isabelle/HOL}},
- booktitle = {Automated Reasoning: second international conference, IJCAR 2004},
- pages = {357--371},
- year = 2004,
- editor = {David Basin and Micha\"el Rusiowitch},
- publisher = {Springer}
-}
-
-@Book{Oberschelp:1993,
- author = {Arnold Oberschelp},
- title = {Rekursionstheorie},
- publisher = {BI-Wissenschafts-Verlag},
- year = 1993
-}
-
-@InProceedings{Podelski-Rybalchenko,
- author = {Andreas Podelski and Andrey Rybalchenko},
- title = {Transition Invariants},
- booktitle = {19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)},
- pages = {32--41},
- year = 2004
-}
-
-@Book{davenport92,
- author = {H. Davenport},
- title = {The Higher Arithmetic},
- publisher = {Cambridge University Press},
- year = 1992
-}
-
-@InProceedings{paulin-tlca,
- author = {Christine Paulin-Mohring},
- title = {Inductive Definitions in the System {Coq}: Rules and
- Properties},
- crossref = {tlca93},
- pages = {328-345}}
-
-@Proceedings{tlca93,
- title = {Typed Lambda Calculi and Applications},
- booktitle = {Typed Lambda Calculi and Applications},
- editor = {M. Bezem and J.F. Groote},
- year = 1993,
- publisher = {Springer},
- series = {LNCS 664}}
--- a/src/HOL/Library/Library/document/root.tex Tue May 25 20:28:16 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage{ifthen}
-\usepackage[latin1]{inputenc}
-\usepackage[english]{babel}
-\usepackage{isabelle,isabellesym,amssymb,stmaryrd}
-\usepackage{pdfsetup}
-
-\urlstyle{rm}
-\isabellestyle{it}
-\pagestyle{myheadings}
-
-\begin{document}
-
-\title{The Supplemental Isabelle/HOL Library}
-\author{}
-\maketitle
-
-\tableofcontents
-\newpage
-
-\renewcommand{\isamarkupheader}[1]%
-{\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}%
-\markright{THEORY~``\isabellecontext''}}
-\renewcommand{\isasymguillemotright}{$\gg$}
-
-\input{session}
-
-\pagestyle{headings}
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/document/root.bib Tue May 25 21:49:44 2010 +0200
@@ -0,0 +1,54 @@
+
+@Unpublished{Abrial-Laffitte,
+ author = {Abrial and Laffitte},
+ title = {Towards the Mechanization of the Proofs of
+ Some Classical Theorems of Set Theory},
+ note = {Unpublished}
+}
+
+@InProceedings{Avigad-Donnelly,
+ author = {Jeremy Avigad and Kevin Donnelly},
+ title = {Formalizing {O} notation in {Isabelle/HOL}},
+ booktitle = {Automated Reasoning: second international conference, IJCAR 2004},
+ pages = {357--371},
+ year = 2004,
+ editor = {David Basin and Micha\"el Rusiowitch},
+ publisher = {Springer}
+}
+
+@Book{Oberschelp:1993,
+ author = {Arnold Oberschelp},
+ title = {Rekursionstheorie},
+ publisher = {BI-Wissenschafts-Verlag},
+ year = 1993
+}
+
+@InProceedings{Podelski-Rybalchenko,
+ author = {Andreas Podelski and Andrey Rybalchenko},
+ title = {Transition Invariants},
+ booktitle = {19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)},
+ pages = {32--41},
+ year = 2004
+}
+
+@Book{davenport92,
+ author = {H. Davenport},
+ title = {The Higher Arithmetic},
+ publisher = {Cambridge University Press},
+ year = 1992
+}
+
+@InProceedings{paulin-tlca,
+ author = {Christine Paulin-Mohring},
+ title = {Inductive Definitions in the System {Coq}: Rules and
+ Properties},
+ crossref = {tlca93},
+ pages = {328-345}}
+
+@Proceedings{tlca93,
+ title = {Typed Lambda Calculi and Applications},
+ booktitle = {Typed Lambda Calculi and Applications},
+ editor = {M. Bezem and J.F. Groote},
+ year = 1993,
+ publisher = {Springer},
+ series = {LNCS 664}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/document/root.tex Tue May 25 21:49:44 2010 +0200
@@ -0,0 +1,32 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{ifthen}
+\usepackage[latin1]{inputenc}
+\usepackage[english]{babel}
+\usepackage{isabelle,isabellesym,amssymb,stmaryrd}
+\usepackage{pdfsetup}
+
+\urlstyle{rm}
+\isabellestyle{it}
+\pagestyle{myheadings}
+
+\begin{document}
+
+\title{The Supplemental Isabelle/HOL Library}
+\author{}
+\maketitle
+
+\tableofcontents
+\newpage
+
+\renewcommand{\isamarkupheader}[1]%
+{\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}%
+\markright{THEORY~``\isabellecontext''}}
+\renewcommand{\isasymguillemotright}{$\gg$}
+
+\input{session}
+
+\pagestyle{headings}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}