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
wenzelm@7761
     1
wenzelm@7761
     2
%% $Id$
wenzelm@7748
     3
wenzelm@7748
     4
\documentclass[11pt,a4paper]{article}
wenzelm@10146
     5
\usepackage{ifthen,proof,isabelle,isabellesym}
wenzelm@10146
     6
\usepackage{pdfsetup}\urlstyle{rm}
wenzelm@7748
     7
wenzelm@7748
     8
\renewcommand{\isamarkupheader}[1]{\section{#1}}
wenzelm@7748
     9
wenzelm@10146
    10
\renewcommand{\isacommand}[1]
wenzelm@10146
    11
{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
wenzelm@10146
    12
  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
wenzelm@10146
    13
wenzelm@10146
    14
\newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}}
wenzelm@10146
    15
\newcommand{\dummyproof}{$\DUMMYPROOF$}
wenzelm@10146
    16
wenzelm@7833
    17
\newcommand{\name}[1]{\textsl{#1}}
wenzelm@7748
    18
wenzelm@7748
    19
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
wenzelm@7874
    20
\newcommand{\var}[1]{{?\!\idt{#1}}}
wenzelm@7748
    21
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
wenzelm@7748
    22
\newcommand{\dsh}{\dshsym}
wenzelm@7748
    23
wenzelm@7748
    24
\newcommand{\To}{\to}
wenzelm@7748
    25
\newcommand{\dt}{{\mathpunct.}}
wenzelm@7748
    26
\newcommand{\ap}{\mathbin{\!}}
wenzelm@7748
    27
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
wenzelm@7748
    28
\newcommand{\all}[1]{\forall #1\dt\;}
wenzelm@7748
    29
\newcommand{\ex}[1]{\exists #1\dt\;}
wenzelm@7817
    30
\newcommand{\impl}{\rightarrow}
wenzelm@7817
    31
\newcommand{\conj}{\land}
wenzelm@7833
    32
\newcommand{\disj}{\lor}
wenzelm@7968
    33
\newcommand{\Impl}{\Longrightarrow}
wenzelm@7817
    34
wenzelm@8020
    35
\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
wenzelm@8020
    36
wenzelm@8020
    37
wenzelm@7748
    38
%%% Local Variables: 
wenzelm@7748
    39
%%% mode: latex
wenzelm@7748
    40
%%% TeX-master: "root"
wenzelm@7748
    41
%%% End: