src/HOL/Isar_examples/document/style.tex
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10146 e89309dde9d3
child 18193 54419506df9e
permissions -rw-r--r--
improved theory reference in comment
     1 
     2 %% $Id$
     3 
     4 \documentclass[11pt,a4paper]{article}
     5 \usepackage{ifthen,proof,isabelle,isabellesym}
     6 \usepackage{pdfsetup}\urlstyle{rm}
     7 
     8 \renewcommand{\isamarkupheader}[1]{\section{#1}}
     9 
    10 \renewcommand{\isacommand}[1]
    11 {\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
    12   {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
    13 
    14 \newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}}
    15 \newcommand{\dummyproof}{$\DUMMYPROOF$}
    16 
    17 \newcommand{\name}[1]{\textsl{#1}}
    18 
    19 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
    20 \newcommand{\var}[1]{{?\!\idt{#1}}}
    21 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
    22 \newcommand{\dsh}{\dshsym}
    23 
    24 \newcommand{\To}{\to}
    25 \newcommand{\dt}{{\mathpunct.}}
    26 \newcommand{\ap}{\mathbin{\!}}
    27 \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
    28 \newcommand{\all}[1]{\forall #1\dt\;}
    29 \newcommand{\ex}[1]{\exists #1\dt\;}
    30 \newcommand{\impl}{\rightarrow}
    31 \newcommand{\conj}{\land}
    32 \newcommand{\disj}{\lor}
    33 \newcommand{\Impl}{\Longrightarrow}
    34 
    35 \newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
    36 
    37 
    38 %%% Local Variables: 
    39 %%% mode: latex
    40 %%% TeX-master: "root"
    41 %%% End: