wneuper/isa: doc-src/IsarRef/isar-ref.tex@20e3616b2d9c

     1 \documentclass[12pt,a4paper,fleqn]{report}

     2 \usepackage{amssymb}

     3 \usepackage[greek,english]{babel}

     4 \usepackage[latin1]{inputenc}

     5 \usepackage[only,bigsqcap]{stmaryrd}

     6 \usepackage{textcomp}

     7 \usepackage{latexsym}

     8 \usepackage{graphicx}

     9 \let\intorig=\int  %iman.sty redefines \int

    10 \usepackage{../iman,../extra,../isar,../proof}

    11 \usepackage[nohyphen,strings]{../underscore}

    12 \usepackage{../isabelle,../isabellesym}

    13 \usepackage{../ttbox,,../rail,../railsetup}

    14 \usepackage{supertabular}

    15 \usepackage{style}

    16 \usepackage{../pdfsetup}

    18 \hyphenation{Isabelle}

    19 \hyphenation{Isar}

    21 \isadroptag{theory}

    22 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}

    23 \author{\emph{Makarius Wenzel} \\[3ex]

    24   With Contributions by

    25   Clemens Ballarin,

    26   Stefan Berghofer, \\

    27   Timothy Bourke,

    28   Lucas Dixon,

    29   Florian Haftmann, \\

    30   Gerwin Klein,

    31   Alexander Krauss,

    32   Tobias Nipkow, \\

    33   David von Oheimb,

    34   Larry Paulson,

    35   and Sebastian Skalberg

    36 }

    38 \makeindex

    40 \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}

    41 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}

    42 \railterm{name,nameref,text,type,term,prop,atom}

    44 \railalias{ident}{\railtok{ident}}

    45 \railalias{longident}{\railtok{longident}}

    46 \railalias{symident}{\railtok{symident}}

    47 \railalias{var}{\railtok{var}}

    48 \railalias{textvar}{\railtok{textvar}}

    49 \railalias{typefree}{\railtok{typefree}}

    50 \railalias{typevar}{\railtok{typevar}}

    51 \railalias{nat}{\railtok{nat}}

    52 \railalias{string}{\railtok{string}}

    53 \railalias{verbatim}{\railtok{verbatim}}

    54 \railalias{keyword}{\railtok{keyword}}

    56 \railalias{name}{\railqtok{name}}

    57 \railalias{nameref}{\railqtok{nameref}}

    58 \railalias{text}{\railqtok{text}}

    59 \railalias{type}{\railqtok{type}}

    60 \railalias{term}{\railqtok{term}}

    61 \railalias{prop}{\railqtok{prop}}

    62 \railalias{atom}{\railqtok{atom}}

    64 \railalias{subseteq}{\isasymsubseteq}\railterm{subseteq}

    65 \railalias{equiv}{\isasymequiv}\railterm{equiv}

    66 \railalias{rightleftharpoons}{\isasymrightleftharpoons}\railterm{rightleftharpoons}

    67 \railalias{rightharpoonup}{\isasymrightharpoonup}\railterm{rightharpoonup}

    68 \railalias{leftharpoondown}{\isasymleftharpoondown}\railterm{leftharpoondown}

    69 \railalias{verblbrace}{\texttt{\ttlbrace*}}\railterm{verblbrace}

    70 \railalias{verbrbrace}{\texttt{*\ttrbrace}}\railterm{verbrbrace}

    73 \chardef\charbackquote=`\`

    74 \newcommand{\backquote}{\mbox{\tt\charbackquote}}

    77 \begin{document}

    79 \maketitle

    81 \pagenumbering{roman} \tableofcontents \clearfirst

    83 \part{Basic Concepts}

    84 \input{Thy/document/Introduction.tex}

    85 \input{Thy/document/Framework.tex}

    86 \input{Thy/document/First_Order_Logic.tex}

    87 \part{General Language Elements}

    88 \input{Thy/document/Outer_Syntax.tex}

    89 \input{Thy/document/Document_Preparation.tex}

    90 \input{Thy/document/Spec.tex}

    91 \input{Thy/document/Proof.tex}

    92 \input{Thy/document/Inner_Syntax.tex}

    93 \input{Thy/document/Misc.tex}

    94 \input{Thy/document/Generic.tex}

    95 \part{Object-Logics}

    96 \input{Thy/document/HOL_Specific.tex}

    97 \input{Thy/document/HOLCF_Specific.tex}

    98 \input{Thy/document/ZF_Specific.tex}

   100 \part{Appendix}

   101 \appendix

   102 \input{Thy/document/Quick_Reference.tex}

   103 \let\int\intorig

   104 \input{Thy/document/Symbols.tex}

   105 \input{Thy/document/ML_Tactic.tex}

   107 \begingroup

   108   \bibliographystyle{abbrv} \small\raggedright\frenchspacing

   109   \bibliography{../manual}

   110 \endgroup

   112 \printindex

   114 \end{document}

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 30569	696f93184f0d
child 41179	7d88ebdce380
permissions	-rw-r--r--