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