
wenzelm@7046: 
wenzelm@7046: %% $Id$
wenzelm@7046: 
wenzelm@7836: \documentclass[12pt,a4paper,fleqn]{report}
wenzelm@26738: \usepackage{latexsym,graphicx}
wenzelm@26738: \usepackage{../iman,../extra,../isar,../proof}
wenzelm@26738: \usepackage{Thy/document/isabelle,Thy/document/isabellesym}
wenzelm@26738: \usepackage{../ttbox,,../rail,../railsetup}
wenzelm@26738: \usepackage{style}
wenzelm@26738: \usepackage{../pdfsetup}
wenzelm@7046: 
wenzelm@26741: \hyphenation{Isabelle}
wenzelm@26741: \hyphenation{Isar}
wenzelm@26741: 
wenzelm@26741: \isadroptag{theory}
wenzelm@7046: \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
wenzelm@7050: \author{\emph{Markus Wenzel} \\ TU M\"unchen}
wenzelm@7046: 
wenzelm@7050: \makeindex
wenzelm@7050: 
wenzelm@9204: \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
wenzelm@7167: \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
wenzelm@8596: \railterm{name,nameref,text,type,term,prop,atom}
wenzelm@7134: 
wenzelm@13048: \railalias{ident}{\railtok{ident}}
wenzelm@13048: \railalias{longident}{\railtok{longident}}
wenzelm@13048: \railalias{symident}{\railtok{symident}}
wenzelm@13048: \railalias{var}{\railtok{var}}
wenzelm@13048: \railalias{textvar}{\railtok{textvar}}
wenzelm@13048: \railalias{typefree}{\railtok{typefree}}
wenzelm@13048: \railalias{typevar}{\railtok{typevar}}
wenzelm@13048: \railalias{nat}{\railtok{nat}}
wenzelm@13048: \railalias{string}{\railtok{string}}
wenzelm@13048: \railalias{verbatim}{\railtok{verbatim}}
wenzelm@13048: \railalias{keyword}{\railtok{keyword}}
wenzelm@8594: 
wenzelm@13048: \railalias{name}{\railqtok{name}}
wenzelm@13048: \railalias{nameref}{\railqtok{nameref}}
wenzelm@13048: \railalias{text}{\railqtok{text}}
wenzelm@13048: \railalias{type}{\railqtok{type}}
wenzelm@13048: \railalias{term}{\railqtok{term}}
wenzelm@13048: \railalias{prop}{\railqtok{prop}}
wenzelm@13048: \railalias{atom}{\railqtok{atom}}
wenzelm@7134: 
wenzelm@26786: \railalias{subseteq}{\isasymsubseteq}\railterm{subseteq}
wenzelm@26786: \railalias{equiv}{\isasymequiv}\railterm{equiv}
wenzelm@26786: \railalias{rightleftharpoons}{\isasymrightleftharpoons}\railterm{rightleftharpoons}
wenzelm@26786: \railalias{rightharpoonup}{\isasymrightharpoonup}\railterm{rightharpoonup}
wenzelm@26786: \railalias{leftharpoondown}{\isasymleftharpoondown}\railterm{leftharpoondown}
wenzelm@26786: 
wenzelm@18021: \chardef\charbackquote=`\`
wenzelm@18021: \newcommand{\backquote}{\mbox{\tt\charbackquote}}
wenzelm@18021: 
wenzelm@7895: \newcommand{\drv}{\mathrel{\vdash}}
wenzelm@7895: \newcommand{\edrv}{\mathop{\drv}\nolimits}
wenzelm@7974: \newcommand{\Or}{\mathrel{\;|\;}}
wenzelm@7895: 
wenzelm@10858: \renewcommand{\vec}[1]{\overline{#1}}
wenzelm@7046: 
wenzelm@7046: \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
wenzelm@7046: 
wenzelm@7046: \pagestyle{headings}
wenzelm@7046: \sloppy
wenzelm@7046: \binperiod     %%%treat . like a binary operator
wenzelm@7046: 
wenzelm@7134: \renewcommand{\phi}{\varphi}
wenzelm@7046: 
wenzelm@7046: 
wenzelm@7046: \begin{document}
wenzelm@7046: 
wenzelm@7046: \underscoreoff
wenzelm@7046: 
wenzelm@7046: \maketitle 
wenzelm@7046: 
wenzelm@7046: \pagenumbering{roman} \tableofcontents \clearfirst
wenzelm@7046: 
wenzelm@26741: \input{Thy/document/intro.tex}
wenzelm@26741: \input{basics.tex}
wenzelm@26754: \input{Thy/document/syntax.tex}
wenzelm@26767: \input{Thy/document/pure.tex}
wenzelm@26782: \input{Thy/document/Generic.tex}
wenzelm@26840: \input{Thy/document/HOL_Specific.tex}
wenzelm@26840: \input{Thy/document/HOLCF_Specific.tex}
wenzelm@26840: \input{Thy/document/ZF_Specific.tex}
wenzelm@26741: \input{logics.tex}
wenzelm@7046: 
wenzelm@7895: \appendix
wenzelm@26779: \input{Thy/document/Quick_Reference.tex}
wenzelm@26741: \input{conversion.tex}
wenzelm@7895: 
wenzelm@7046: \begingroup
wenzelm@7046:   \bibliographystyle{plain} \small\raggedright\frenchspacing
wenzelm@7046:   \bibliography{../manual}
wenzelm@7046: \endgroup
wenzelm@7046: 
wenzelm@8828: \printindex
wenzelm@7046: 
wenzelm@7046: \end{document}




