--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Logics-ZF/document/root.tex Sat Apr 05 11:37:00 2014 +0200
@@ -0,0 +1,91 @@
+\documentclass[11pt,a4paper]{report}
+\usepackage{isabelle,isabellesym,railsetup}
+\usepackage{graphicx,logics,ttbox,proof,latexsym}
+\usepackage{isar}
+
+\usepackage{pdfsetup}
+%last package!
+
+\remarkstrue
+
+%%% 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_zf} \\[4ex]
+ Isabelle's Logics: FOL and ZF}
+
+\author{{\em Lawrence C. Paulson}\\
+ Computer Laboratory \\ University of Cambridge \\
+ \texttt{lcp@cl.cam.ac.uk}\\[3ex]
+ With Contributions by Tobias Nipkow and Markus Wenzel}
+
+\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
+ \hrule\bigskip}
+\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
+
+\let\ts=\thinspace
+
+\makeindex
+
+\underscoreoff
+
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
+
+\pagestyle{headings}
+\sloppy
+\binperiod %%%treat . like a binary operator
+
+
+\isadroptag{theory}
+
+\railtermfont{\isabellestyle{tt}}
+\railnontermfont{\isabellestyle{literal}}
+\railnamefont{\isabellestyle{literal}}
+
+
+\begin{document}
+\maketitle
+
+\begin{abstract}
+This manual describes Isabelle's formalizations of many-sorted first-order
+logic (\texttt{FOL}) and Zermelo-Fraenkel set theory (\texttt{ZF}). See the
+\emph{Reference Manual} for general Isabelle commands, and \emph{Introduction
+ to Isabelle} for an overall tutorial.
+
+This manual is part of the earlier Isabelle documentation,
+which is somewhat superseded by the Isabelle/HOL
+\emph{Tutorial}~\cite{isa-tutorial}. However, the present document is the
+only available documentation for Isabelle's versions of first-order logic
+and set theory. Much of it is concerned with
+the primitives for conducting proofs
+using the ML top level. It has been rewritten to use the Isar proof
+language, but evidence of the old \ML{} orientation remains.
+\end{abstract}
+
+
+\subsubsection*{Acknowledgements}
+Markus Wenzel made numerous improvements.
+ Philippe de Groote contributed to~ZF. Philippe No\"el and
+ Martin Coen made many contributions to~ZF. The research has
+ been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
+ GR/K77051, GR/M75440) and by ESPRIT (projects 3245:
+ Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
+ \emph{Deduktion}.
+
+\pagenumbering{roman} \tableofcontents \cleardoublepage
+\pagenumbering{arabic}
+\setcounter{page}{1}
+\input{syntax}
+\input{FOL}
+\input{ZF}
+
+\isabellestyle{literal}
+\input{ZF_Isar}
+\isabellestyle{tt}
+
+\bibliographystyle{plain}
+\bibliography{manual}
+\printindex
+\end{document}