wenzelm@7836: \documentclass[12pt,a4paper,fleqn]{report}
wenzelm@28838: \usepackage{amssymb}
wenzelm@28838: \usepackage[greek,english]{babel}
wenzelm@28838: \usepackage[latin1]{inputenc}
wenzelm@28838: \usepackage[only,bigsqcap]{stmaryrd}
wenzelm@28838: \usepackage{textcomp}
wenzelm@28838: \usepackage{latexsym}
wenzelm@28838: \usepackage{graphicx}
wenzelm@28838: \let\intorig=\int  %iman.sty redefines \int
wenzelm@26738: \usepackage{../iman,../extra,../isar,../proof}
wenzelm@26862: \usepackage[nohyphen,strings]{../underscore}
wenzelm@26906: \usepackage{../isabelle,../isabellesym}
wenzelm@26738: \usepackage{../ttbox,,../rail,../railsetup}
wenzelm@28773: \usepackage{supertabular}
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@26870: \author{\emph{Makarius Wenzel} \\[3ex]
wenzelm@26870:   With Contributions by
wenzelm@26870:   Clemens Ballarin,
wenzelm@26870:   Stefan Berghofer, \\
haftmann@30569:   Timothy Bourke,
wenzelm@27038:   Lucas Dixon,
wenzelm@30185:   Florian Haftmann, \\
wenzelm@30185:   Gerwin Klein,
wenzelm@27038:   Alexander Krauss,
wenzelm@30185:   Tobias Nipkow, \\
wenzelm@30185:   David von Oheimb,
wenzelm@27038:   Larry Paulson,
wenzelm@26870:   and Sebastian Skalberg
wenzelm@26870: }
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@26848: \railalias{verblbrace}{\texttt{\ttlbrace*}}\railterm{verblbrace}
wenzelm@26848: \railalias{verbrbrace}{\texttt{*\ttrbrace}}\railterm{verbrbrace}
wenzelm@26848: 
wenzelm@26786: 
wenzelm@18021: \chardef\charbackquote=`\`
wenzelm@18021: \newcommand{\backquote}{\mbox{\tt\charbackquote}}
wenzelm@18021: 
wenzelm@7046: 
wenzelm@7046: \begin{document}
wenzelm@7046: 
wenzelm@7046: \maketitle 
wenzelm@7046: 
wenzelm@7046: \pagenumbering{roman} \tableofcontents \clearfirst
wenzelm@7046: 
wenzelm@30044: \part{Basic Concepts}
wenzelm@27035: \input{Thy/document/Introduction.tex}
wenzelm@30042: \input{Thy/document/Framework.tex}
wenzelm@30056: \input{Thy/document/First_Order_Logic.tex}
wenzelm@30044: \part{General Language Elements}
wenzelm@27037: \input{Thy/document/Outer_Syntax.tex}
wenzelm@28751: \input{Thy/document/Document_Preparation.tex}
wenzelm@26869: \input{Thy/document/Spec.tex}
wenzelm@26869: \input{Thy/document/Proof.tex}
wenzelm@28762: \input{Thy/document/Inner_Syntax.tex}
wenzelm@27048: \input{Thy/document/Misc.tex}
wenzelm@26782: \input{Thy/document/Generic.tex}
wenzelm@30044: \part{Object-Logics}
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@7046: 
wenzelm@30044: \part{Appendix}
wenzelm@7895: \appendix
wenzelm@26779: \input{Thy/document/Quick_Reference.tex}
wenzelm@28838: \let\int\intorig
wenzelm@28838: \input{Thy/document/Symbols.tex}
wenzelm@26846: \input{Thy/document/ML_Tactic.tex}
wenzelm@7895: 
wenzelm@7046: \begingroup
wenzelm@30114:   \bibliographystyle{abbrv} \small\raggedright\frenchspacing
wenzelm@7046:   \bibliography{../manual}
wenzelm@7046: \endgroup
wenzelm@7046: 
wenzelm@8828: \printindex
wenzelm@7046: 
wenzelm@7046: \end{document}