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

     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   Lucas Dixon,

    28   Florian Haftmann,

    29   Gerwin Klein, \\

    30   Alexander Krauss,

    31   Tobias Nipkow,

    32   David von Oheimb, \\

    33   Larry Paulson,

    34   and Sebastian Skalberg

    35 }

    37 \makeindex

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

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

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

    43 \railalias{ident}{\railtok{ident}}

    44 \railalias{longident}{\railtok{longident}}

    45 \railalias{symident}{\railtok{symident}}

    46 \railalias{var}{\railtok{var}}

    47 \railalias{textvar}{\railtok{textvar}}

    48 \railalias{typefree}{\railtok{typefree}}

    49 \railalias{typevar}{\railtok{typevar}}

    50 \railalias{nat}{\railtok{nat}}

    51 \railalias{string}{\railtok{string}}

    52 \railalias{verbatim}{\railtok{verbatim}}

    53 \railalias{keyword}{\railtok{keyword}}

    55 \railalias{name}{\railqtok{name}}

    56 \railalias{nameref}{\railqtok{nameref}}

    57 \railalias{text}{\railqtok{text}}

    58 \railalias{type}{\railqtok{type}}

    59 \railalias{term}{\railqtok{term}}

    60 \railalias{prop}{\railqtok{prop}}

    61 \railalias{atom}{\railqtok{atom}}

    63 \railalias{subseteq}{\isasymsubseteq}\railterm{subseteq}

    64 \railalias{equiv}{\isasymequiv}\railterm{equiv}

    65 \railalias{rightleftharpoons}{\isasymrightleftharpoons}\railterm{rightleftharpoons}

    66 \railalias{rightharpoonup}{\isasymrightharpoonup}\railterm{rightharpoonup}

    67 \railalias{leftharpoondown}{\isasymleftharpoondown}\railterm{leftharpoondown}

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

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

    72 \chardef\charbackquote=`\`

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

    76 \begin{document}

    78 \maketitle

    80 \pagenumbering{roman} \tableofcontents \clearfirst

    82 \part{Basic Concepts}

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

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

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

    86 \part{General Language Elements}

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

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

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

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

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

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

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

    94 \part{Object-Logics}

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

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

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

    99 \part{Appendix}

   100 \appendix

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

   102 \let\int\intorig

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

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

   106 \begingroup

   107   \bibliographystyle{plain} \small\raggedright\frenchspacing

   108   \bibliography{../manual}

   109 \endgroup

   111 \printindex

   113 \end{document}

author	wenzelm
	Thu, 12 Feb 2009 11:19:12 +0100
changeset 30056	924c1fd5f303
parent 30044	cf48beb23a70
child 30114	1fb1833cb199
permissions	-rw-r--r--