# HG changeset patch
# User wenzelm
# Date 1011363467 -3600
# Node ID 894da6aee971e11c4f8515c274af386d1618a924
# Parent  76f3dd2f151af7fa0d02380f800d68bd0bf4b17d
moved document sources to proper place, *within* Library/Library (!);

diff -r 76f3dd2f151a -r 894da6aee971 src/HOL/Library/Library/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Library/document/root.bib	Fri Jan 18 15:17:47 2002 +0100
@@ -0,0 +1,22 @@
+
+@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 76f3dd2f151a -r 894da6aee971 src/HOL/Library/Library/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Library/document/root.tex	Fri Jan 18 15:17:47 2002 +0100
@@ -0,0 +1,46 @@
+
+% $Id$
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{ifthen}
+\usepackage{isabelle,isabellesym,pdfsetup}
+
+\urlstyle{rm}
+\isabellestyle{it}
+\pagestyle{myheadings}
+
+\begin{document}
+
+\title{The Supplemental Isabelle/HOL Library}
+\author{
+  Gertrud Bauer \\
+  Tobias Nipkow \\
+  David von Oheimb \\
+  Lawrence C Paulson \\
+  Thomas M Rasmussen \\
+  Christophe Tabacznyj \\
+  Markus Wenzel}
+\maketitle
+
+\tableofcontents
+\newpage
+
+%now hack the "header" markup to support \title and \author
+\newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}}
+\newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}}
+\renewcommand{\isamarkupheader}[1]%
+{\title{***~Theory ``\isabellecontext'': unknown title}\author{}%
+#1%
+\ifthenelse{\equal{}{\isabelletitle}}{}{\newpage\section{\isabelletitle}}%
+\markright{THEORY~``\isabellecontext''}%
+\ifthenelse{\equal{}{\isabelleauthor}}{}%
+{{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}
+
+\parindent 0pt \parskip 0.5ex
+\input{session}
+
+\pagestyle{headings}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
diff -r 76f3dd2f151a -r 894da6aee971 src/HOL/Library/document/root.bib
--- a/src/HOL/Library/document/root.bib	Thu Jan 17 21:07:11 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-
-@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 76f3dd2f151a -r 894da6aee971 src/HOL/Library/document/root.tex
--- a/src/HOL/Library/document/root.tex	Thu Jan 17 21:07:11 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-
-% $Id$
-
-\documentclass[11pt,a4paper]{article}
-\usepackage{ifthen}
-\usepackage{isabelle,isabellesym,pdfsetup}
-
-\urlstyle{rm}
-\isabellestyle{it}
-\pagestyle{myheadings}
-
-\begin{document}
-
-\title{The Supplemental Isabelle/HOL Library}
-\author{
-  Gertrud Bauer \\
-  Tobias Nipkow \\
-  David von Oheimb \\
-  Lawrence C Paulson \\
-  Thomas M Rasmussen \\
-  Christophe Tabacznyj \\
-  Markus Wenzel}
-\maketitle
-
-\tableofcontents
-\newpage
-
-%now hack the "header" markup to support \title and \author
-\newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}}
-\newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}}
-\renewcommand{\isamarkupheader}[1]%
-{\title{***~Theory ``\isabellecontext'': unknown title}\author{}%
-#1%
-\ifthenelse{\equal{}{\isabelletitle}}{}{\newpage\section{\isabelletitle}}%
-\markright{THEORY~``\isabellecontext''}%
-\ifthenelse{\equal{}{\isabelleauthor}}{}%
-{{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}
-
-\parindent 0pt \parskip 0.5ex
-\input{session}
-
-\pagestyle{headings}
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}