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

     2 %% $Id$

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

     5 \usepackage{amssymb}

     6 \usepackage[greek,english]{babel}

     7 \usepackage[latin1]{inputenc}

     8 \usepackage[only,bigsqcap]{stmaryrd}

     9 \usepackage{textcomp}

    10 \usepackage{latexsym}

    11 \usepackage{graphicx}

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

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

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

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

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

    17 \usepackage{supertabular}

    18 \usepackage{style}

    19 \usepackage{../pdfsetup}

    21 \hyphenation{Isabelle}

    22 \hyphenation{Isar}

    24 \isadroptag{theory}

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

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

    27   With Contributions by

    28   Clemens Ballarin,

    29   Stefan Berghofer, \\

    30   Lucas Dixon,

    31   Florian Haftmann,

    32   Gerwin Klein, \\

    33   Alexander Krauss,

    34   Tobias Nipkow,

    35   David von Oheimb, \\

    36   Larry Paulson,

    37   and Sebastian Skalberg

    38 }

    40 \makeindex

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

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

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

    46 \railalias{ident}{\railtok{ident}}

    47 \railalias{longident}{\railtok{longident}}

    48 \railalias{symident}{\railtok{symident}}

    49 \railalias{var}{\railtok{var}}

    50 \railalias{textvar}{\railtok{textvar}}

    51 \railalias{typefree}{\railtok{typefree}}

    52 \railalias{typevar}{\railtok{typevar}}

    53 \railalias{nat}{\railtok{nat}}

    54 \railalias{string}{\railtok{string}}

    55 \railalias{verbatim}{\railtok{verbatim}}

    56 \railalias{keyword}{\railtok{keyword}}

    58 \railalias{name}{\railqtok{name}}

    59 \railalias{nameref}{\railqtok{nameref}}

    60 \railalias{text}{\railqtok{text}}

    61 \railalias{type}{\railqtok{type}}

    62 \railalias{term}{\railqtok{term}}

    63 \railalias{prop}{\railqtok{prop}}

    64 \railalias{atom}{\railqtok{atom}}

    66 \railalias{subseteq}{\isasymsubseteq}\railterm{subseteq}

    67 \railalias{equiv}{\isasymequiv}\railterm{equiv}

    68 \railalias{rightleftharpoons}{\isasymrightleftharpoons}\railterm{rightleftharpoons}

    69 \railalias{rightharpoonup}{\isasymrightharpoonup}\railterm{rightharpoonup}

    70 \railalias{leftharpoondown}{\isasymleftharpoondown}\railterm{leftharpoondown}

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

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

    75 \chardef\charbackquote=`\`

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

    79 \begin{document}

    81 \maketitle

    83 \pagenumbering{roman} \tableofcontents \clearfirst

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

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

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

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

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

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

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

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

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

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

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

    97 \appendix

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

    99 \let\int\intorig

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

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

   103 \begingroup

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

   105   \bibliography{../manual}

   106 \endgroup

   108 \printindex

   110 \end{document}

author	wenzelm
	Tue, 18 Nov 2008 18:25:10 +0100
changeset 28838	d5db6dfcb34a
parent 28773	39b4cedb8433
child 30042	b6266c4c68fe
child 30240	5b25fee0362c
permissions	-rw-r--r--