--- a/doc-src/HOL/logics-HOL.tex Mon Aug 27 21:30:18 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-\documentclass[12pt,a4paper]{report}
-\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
-\usepackage{graphicx,../iman,../extra,../ttbox,../proof,latexsym,../pdfsetup}
-
-%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
-%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
-%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
-%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
-
-
-\title{\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
- Isabelle's Logics: HOL%
- \thanks{The research has been funded by the EPSRC (grants GR/G53279,
- GR\slash H40570, GR/K57381, GR/K77051, GR/M75440), by ESPRIT (projects 3245:
- Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
- \emph{Deduktion}.}}
-
-\author{Tobias Nipkow\footnote
-{Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
- \texttt{nipkow@in.tum.de}} and
-Lawrence C. Paulson\footnote
-{Computer Laboratory, University of Cambridge, \texttt{lcp@cl.cam.ac.uk}} and
-Markus Wenzel\footnote
-{Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
- \texttt{wenzelm@in.tum.de}}}
-
-\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
- \hrule\bigskip}
-\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
-
-\newcommand\bs{\char '134 } % A backslash character for \tt font
-
-\makeindex
-
-\underscoreoff
-
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
-
-\pagestyle{headings}
-\sloppy
-\binperiod %%%treat . like a binary operator
-
-\begin{document}
-\maketitle
-
-\begin{abstract}
- This manual describes Isabelle's formalization of Higher-Order Logic, a
- polymorphic version of Church's Simple Theory of Types. HOL can be best
- understood as a simply-typed version of classical set theory. The monograph
- \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a
- gentle introduction on using Isabelle/HOL in practice.
-\end{abstract}
-
-\pagenumbering{roman} \tableofcontents \clearfirst
-\input{../Logics/syntax}
-\include{HOL}
-\bibliographystyle{plain}
-\bibliography{../manual}
-\printindex
-\end{document}