%
% $Id$
%
%% document setup
\documentclass[12pt,a4paper]{article}
\usepackage{ifthen,latexsym}
%\usepackage[latin1]{inputenc}
%\usepackage[german]{babel}\AtBeginDocument{\mdqon}
\usepackage{isabelle,isabellesym}
\sloppy \parindent 0pt \parskip 1ex
\makeatletter
\@ifundefined{pdfoutput}{\newcommand{\href}[2]{#2}}{}
\makeatother
%borrowed from a4wide/12pt :-(
\oddsidemargin 0 in
\evensidemargin 0 in
\marginparwidth 0.75 in
\textwidth 6.375 true in
\addtolength{\topmargin}{-2cm}
\addtolength{\textheight}{2cm}
\thispagestyle{empty}
\newlength{\TUMBr}\settowidth{\TUMBr}{{\bf Technische Universität München}}
\newcommand{\header}[2]{{\bf
\parbox{0.5\textwidth}{
\parbox{\TUMBr}{\begin{center}
Technische Universität München \\
Institut für Informatik \\
Prof.~Tobias Nipkow, Ph.\,D.\\
Gerwin Klein\end{center}}}
\parbox{0.5\textwidth}{
\begin{flushright}
SS 2002 \\ #1 \\ #2 \\
\end{flushright}}
\bigskip
\begin{center}
\Large
Praktikum Spezifikation und Verifikation
\end{center}
\bigskip}}
\newcommand{\note}[1]{\textbf{$\rhd$~#1}}
\newcommand{\Chref}[1]{Chapter~\ref{#1}}
\newcommand{\chref}[1]{chapter~\ref{#1}}
\newcommand{\Secref}[1]{Section~\ref{#1}}
\newcommand{\secref}[1]{§\ref{#1}}
%% misc macros
\newcommand{\text}[1]{\mbox{#1}}
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
\newcommand{\var}[1]{{?\!\idt{#1}}}
\newcommand{\name}[1]{\textsl{#1}}
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
\newcommand{\dsh}{\dshsym}
\newcommand{\pow}[2]{#1\mathbin{\!\symbol{94}\!}#2}
%\newcommand{\ap}{\mathpalette{\mathbin{\mkern-1mu}}{\mathbin{\mkern-2mu}}{\mathbin{}}{\mathbin{}}}
\newcommand{\ap}{\mathpalette{\mathbin{}}{\mathbin{}}{\mathbin{}}{\mathbin{}}}
\newcommand{\dt}{{\mathpunct.\;}}
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt}
\newcommand{\impl}{\to}
%% tune Isabelle output
\newcommand{\isasorry}{$\;\langle\idt{proof}\rangle$}
\newcommand{\isaoops}{$\vdots$}
\renewcommand{\isacommand}[1]
{\ifthenelse{\equal{sorry}{#1}}{\isasorry}
{\ifthenelse{\equal{oops}{#1}}{\isaoops}{\isakeyword{#1}}}}
\renewcommand{\isabellestyle}{\footnotesize\tt\slshape}
\renewcommand{\isa}[1]{\emph{\small\tt\slshape #1}}
%\renewcommand\isabellemarkupsubsubsection{\subsubsection*}
\renewcommand\isamarkupsubsubsection{\subsubsection*}
\renewcommand{\isamarkupheader}[1]{\subsection*{#1}}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: