# HG changeset patch # User wenzelm # Date 1274816984 -7200 # Node ID ccae4ecd67f445a8c786c911f581ac9129455a5d # Parent 59cee8807c298b992b0176087acef50b3017f8d4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML; diff -r 59cee8807c29 -r ccae4ecd67f4 src/HOL/IsaMakefile --- 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 diff -r 59cee8807c29 -r ccae4ecd67f4 src/HOL/Library/HOL_Library_ROOT.ML --- /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"]; diff -r 59cee8807c29 -r ccae4ecd67f4 src/HOL/Library/Library/ROOT.ML --- 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"]; diff -r 59cee8807c29 -r ccae4ecd67f4 src/HOL/Library/Library/document/root.bib --- 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}} diff -r 59cee8807c29 -r ccae4ecd67f4 src/HOL/Library/Library/document/root.tex --- 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} diff -r 59cee8807c29 -r ccae4ecd67f4 src/HOL/Library/document/root.bib --- /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}} diff -r 59cee8807c29 -r ccae4ecd67f4 src/HOL/Library/document/root.tex --- /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}