|
13739
|
1 |
%
|
|
|
2 |
% $Id$
|
|
|
3 |
%
|
|
|
4 |
|
|
|
5 |
%% document setup
|
|
|
6 |
|
|
|
7 |
\documentclass[12pt,a4paper]{article}
|
|
|
8 |
\usepackage{ifthen,latexsym}
|
|
|
9 |
%\usepackage[latin1]{inputenc}
|
|
|
10 |
%\usepackage[german]{babel}\AtBeginDocument{\mdqon}
|
|
|
11 |
\usepackage{isabelle,isabellesym}
|
|
|
12 |
\sloppy \parindent 0pt \parskip 1ex
|
|
|
13 |
|
|
|
14 |
\makeatletter
|
|
|
15 |
\@ifundefined{pdfoutput}{\newcommand{\href}[2]{#2}}{}
|
|
|
16 |
\makeatother
|
|
|
17 |
|
|
|
18 |
%borrowed from a4wide/12pt :-(
|
|
|
19 |
\oddsidemargin 0 in
|
|
|
20 |
\evensidemargin 0 in
|
|
|
21 |
\marginparwidth 0.75 in
|
|
|
22 |
\textwidth 6.375 true in
|
|
|
23 |
\addtolength{\topmargin}{-2cm}
|
|
|
24 |
\addtolength{\textheight}{2cm}
|
|
|
25 |
|
|
|
26 |
\thispagestyle{empty}
|
|
|
27 |
|
|
|
28 |
\newlength{\TUMBr}\settowidth{\TUMBr}{{\bf Technische Universität München}}
|
|
|
29 |
\newcommand{\header}[2]{{\bf
|
|
|
30 |
\parbox{0.5\textwidth}{
|
|
|
31 |
\parbox{\TUMBr}{\begin{center}
|
|
|
32 |
Technische Universität München \\
|
|
|
33 |
Institut für Informatik \\
|
|
|
34 |
Prof.~Tobias Nipkow, Ph.\,D.\\
|
|
|
35 |
Gerwin Klein\end{center}}}
|
|
|
36 |
\parbox{0.5\textwidth}{
|
|
|
37 |
\begin{flushright}
|
|
|
38 |
SS 2002 \\ #1 \\ #2 \\
|
|
|
39 |
\end{flushright}}
|
|
|
40 |
\bigskip
|
|
|
41 |
\begin{center}
|
|
|
42 |
\Large
|
|
|
43 |
Praktikum Spezifikation und Verifikation
|
|
|
44 |
\end{center}
|
|
|
45 |
\bigskip}}
|
|
|
46 |
|
|
|
47 |
\newcommand{\note}[1]{\textbf{$\rhd$~#1}}
|
|
|
48 |
|
|
|
49 |
|
|
|
50 |
\newcommand{\Chref}[1]{Chapter~\ref{#1}}
|
|
|
51 |
\newcommand{\chref}[1]{chapter~\ref{#1}}
|
|
|
52 |
\newcommand{\Secref}[1]{Section~\ref{#1}}
|
|
|
53 |
\newcommand{\secref}[1]{§\ref{#1}}
|
|
|
54 |
|
|
|
55 |
|
|
|
56 |
%% misc macros
|
|
|
57 |
|
|
|
58 |
\newcommand{\text}[1]{\mbox{#1}}
|
|
|
59 |
|
|
|
60 |
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
|
|
|
61 |
\newcommand{\var}[1]{{?\!\idt{#1}}}
|
|
|
62 |
\newcommand{\name}[1]{\textsl{#1}}
|
|
|
63 |
|
|
|
64 |
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
|
|
|
65 |
\newcommand{\dsh}{\dshsym}
|
|
|
66 |
|
|
|
67 |
\newcommand{\pow}[2]{#1\mathbin{\!\symbol{94}\!}#2}
|
|
|
68 |
|
|
|
69 |
%\newcommand{\ap}{\mathpalette{\mathbin{\mkern-1mu}}{\mathbin{\mkern-2mu}}{\mathbin{}}{\mathbin{}}}
|
|
|
70 |
\newcommand{\ap}{\mathpalette{\mathbin{}}{\mathbin{}}{\mathbin{}}{\mathbin{}}}
|
|
|
71 |
\newcommand{\dt}{{\mathpunct.\;}}
|
|
|
72 |
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt}
|
|
|
73 |
|
|
|
74 |
\newcommand{\impl}{\to}
|
|
|
75 |
|
|
|
76 |
|
|
|
77 |
%% tune Isabelle output
|
|
|
78 |
|
|
|
79 |
\newcommand{\isasorry}{$\;\langle\idt{proof}\rangle$}
|
|
|
80 |
\newcommand{\isaoops}{$\vdots$}
|
|
|
81 |
|
|
|
82 |
\renewcommand{\isacommand}[1]
|
|
|
83 |
{\ifthenelse{\equal{sorry}{#1}}{\isasorry}
|
|
|
84 |
{\ifthenelse{\equal{oops}{#1}}{\isaoops}{\isakeyword{#1}}}}
|
|
|
85 |
|
|
|
86 |
\renewcommand{\isabellestyle}{\footnotesize\tt\slshape}
|
|
|
87 |
\renewcommand{\isa}[1]{\emph{\small\tt\slshape #1}}
|
|
|
88 |
%\renewcommand\isabellemarkupsubsubsection{\subsubsection*}
|
|
|
89 |
\renewcommand\isamarkupsubsubsection{\subsubsection*}
|
|
|
90 |
|
|
|
91 |
\renewcommand{\isamarkupheader}[1]{\subsection*{#1}}
|
|
|
92 |
|
|
|
93 |
|
|
|
94 |
%%% Local Variables:
|
|
|
95 |
%%% mode: latex
|
|
|
96 |
%%% TeX-master: "root"
|
|
|
97 |
%%% End:
|