|
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: |