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