|
7761
|
1 |
|
|
|
2 |
%% $Id$
|
|
7748
|
3 |
|
|
|
4 |
\documentclass[11pt,a4paper]{article}
|
|
7982
|
5 |
\usepackage{comment,proof,isabelle,isabellesym,pdfsetup}
|
|
7748
|
6 |
|
|
|
7 |
\renewcommand{\isamarkupheader}[1]{\section{#1}}
|
|
|
8 |
|
|
7833
|
9 |
\newcommand{\name}[1]{\textsl{#1}}
|
|
7748
|
10 |
|
|
|
11 |
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
|
|
7874
|
12 |
\newcommand{\var}[1]{{?\!\idt{#1}}}
|
|
7748
|
13 |
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
|
|
|
14 |
\newcommand{\dsh}{\dshsym}
|
|
|
15 |
|
|
|
16 |
\newcommand{\To}{\to}
|
|
|
17 |
\newcommand{\dt}{{\mathpunct.}}
|
|
|
18 |
\newcommand{\ap}{\mathbin{\!}}
|
|
|
19 |
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
|
|
|
20 |
\newcommand{\all}[1]{\forall #1\dt\;}
|
|
|
21 |
\newcommand{\ex}[1]{\exists #1\dt\;}
|
|
7817
|
22 |
\newcommand{\impl}{\rightarrow}
|
|
|
23 |
\newcommand{\conj}{\land}
|
|
7833
|
24 |
\newcommand{\disj}{\lor}
|
|
7968
|
25 |
\newcommand{\Impl}{\Longrightarrow}
|
|
7817
|
26 |
|
|
8020
|
27 |
\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
|
|
|
28 |
|
|
|
29 |
|
|
7748
|
30 |
%%% Local Variables:
|
|
|
31 |
%%% mode: latex
|
|
|
32 |
%%% TeX-master: "root"
|
|
|
33 |
%%% End:
|