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