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

     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	blanchet
	Wed, 04 Mar 2009 11:05:29 +0100
changeset 30242	aea5d7fa7ef5
parent 30240	5b25fee0362c
parent 30185	6889bfc03804
child 30569	696f93184f0d
permissions	-rw-r--r--