1\documentclass[12pt,a4paper]{report} 2\usepackage{isabelle,isabellesym} 3\usepackage{graphicx,iman,extra,ttbox,proof,latexsym,pdfsetup} 4 5%%%STILL NEEDS MODAL, LCF 6%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1} 7%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1} 8%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1} 9%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1} 10%% run ../sedindex logics to prepare index file 11\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Isabelle's Logics} 12 13\author{{\em Lawrence C. Paulson}\\ 14 Computer Laboratory \\ University of Cambridge \\ 15 \texttt{lcp@cl.cam.ac.uk}\\[3ex] 16 With Contributions by Tobias Nipkow and Markus Wenzel% 17 \thanks{Markus Wenzel made numerous improvements. Sara Kalvala 18 contributed Chap.\ts\ref{chap:sequents}. Philippe de Groote 19 wrote the first version of the logic~LK. Tobias Nipkow developed 20 LCF and~Cube. Martin Coen developed~Modal with assistance 21 from Rajeev Gor\'e. The research has been funded by the EPSRC 22 (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT 23 (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG 24 Schwerpunktprogramm \emph{Deduktion}.} } 25 26\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip 27 \hrule\bigskip} 28\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} 29 30\newcommand\bs{\char '134 } % A backslash character for \tt font 31 32\makeindex 33 34\underscoreoff 35 36\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}??? 37 38\pagestyle{headings} 39\sloppy 40\binperiod %%%treat . like a binary operator 41 42\begin{document} 43\maketitle 44\pagenumbering{roman} \tableofcontents \clearfirst 45\input{preface} 46\input{syntax} 47\input{HOL} 48\input{LK} 49\input{Sequents} 50%%\input{Modal} 51\input{CTT} 52\bibliographystyle{plain} 53\bibliography{manual} 54\printindex 55\end{document} 56