src/HOL/Isar_examples/document/style.tex
author wenzelm
Tue, 03 Oct 2000 22:36:22 +0200
changeset 10146 e89309dde9d3
parent 9659 b9cf6801f3da
child 18193 54419506df9e
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7761
7fab9592384f improved presentation;
wenzelm
parents: 7748
diff changeset
     1
7fab9592384f improved presentation;
wenzelm
parents: 7748
diff changeset
     2
%% $Id$
7748
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
     3
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
     4
\documentclass[11pt,a4paper]{article}
10146
wenzelm
parents: 9659
diff changeset
     5
\usepackage{ifthen,proof,isabelle,isabellesym}
wenzelm
parents: 9659
diff changeset
     6
\usepackage{pdfsetup}\urlstyle{rm}
7748
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
     7
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
     8
\renewcommand{\isamarkupheader}[1]{\section{#1}}
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
     9
10146
wenzelm
parents: 9659
diff changeset
    10
\renewcommand{\isacommand}[1]
wenzelm
parents: 9659
diff changeset
    11
{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
wenzelm
parents: 9659
diff changeset
    12
  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
wenzelm
parents: 9659
diff changeset
    13
wenzelm
parents: 9659
diff changeset
    14
\newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}}
wenzelm
parents: 9659
diff changeset
    15
\newcommand{\dummyproof}{$\DUMMYPROOF$}
wenzelm
parents: 9659
diff changeset
    16
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7817
diff changeset
    17
\newcommand{\name}[1]{\textsl{#1}}
7748
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    18
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    19
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
7874
180364256231 improved presentation;
wenzelm
parents: 7869
diff changeset
    20
\newcommand{\var}[1]{{?\!\idt{#1}}}
7748
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    21
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    22
\newcommand{\dsh}{\dshsym}
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    23
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    24
\newcommand{\To}{\to}
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    25
\newcommand{\dt}{{\mathpunct.}}
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    26
\newcommand{\ap}{\mathbin{\!}}
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    27
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    28
\newcommand{\all}[1]{\forall #1\dt\;}
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    29
\newcommand{\ex}[1]{\exists #1\dt\;}
7817
76cffd7dff2e improved;
wenzelm
parents: 7800
diff changeset
    30
\newcommand{\impl}{\rightarrow}
76cffd7dff2e improved;
wenzelm
parents: 7800
diff changeset
    31
\newcommand{\conj}{\land}
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7817
diff changeset
    32
\newcommand{\disj}{\lor}
7968
964b65b4e433 improved presentation;
wenzelm
parents: 7874
diff changeset
    33
\newcommand{\Impl}{\Longrightarrow}
7817
76cffd7dff2e improved;
wenzelm
parents: 7800
diff changeset
    34
8020
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents: 7982
diff changeset
    35
\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents: 7982
diff changeset
    36
2823ce1753a5 added Isar_examples/Puzzle.thy;
wenzelm
parents: 7982
diff changeset
    37
7748
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    38
%%% Local Variables: 
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    39
%%% mode: latex
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    40
%%% TeX-master: "root"
5b9c45b21782 improved presentation;
wenzelm
parents:
diff changeset
    41
%%% End: