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

     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	haftmann
	Wed, 18 Mar 2009 11:57:28 +0100
changeset 30569	696f93184f0d
parent 30242	aea5d7fa7ef5
child 41179	7d88ebdce380
permissions	-rw-r--r--