equal
deleted
inserted
replaced
1 \documentclass[11pt]{report} |
1 \documentclass[11pt]{report} |
2 \usepackage{a4,latexsym,verbatim} |
2 \usepackage{a4,latexsym,verbatim,graphicx,../pdfsetup} |
3 \usepackage{graphicx} |
3 |
4 |
4 |
5 \makeatletter |
5 \makeatletter |
6 \input{../iman.sty} |
6 \input{../iman.sty} |
7 \input{extra.sty} |
7 \input{extra.sty} |
8 \makeatother |
8 \makeatother |
37 \pagestyle{headings} |
37 \pagestyle{headings} |
38 %\sloppy |
38 %\sloppy |
39 %\binperiod %%%treat . like a binary operator |
39 %\binperiod %%%treat . like a binary operator |
40 |
40 |
41 \begin{document} |
41 \begin{document} |
42 \title{\includegraphics[scale=.8]{isabelle_hol.eps} |
42 \title{\includegraphics[scale=.8]{isabelle_hol} |
43 \\ \vspace{0.5cm} The Tutorial |
43 \\ \vspace{0.5cm} The Tutorial |
44 \\ --- DRAFT ---} |
44 \\ --- DRAFT ---} |
45 \author{Tobias Nipkow\\ |
45 \author{Tobias Nipkow\\ |
46 Technische Universit\"at M\"unchen \\ |
46 Technische Universit\"at M\"unchen \\ |
47 Institut f\"ur Informatik \\ |
47 Institut f\"ur Informatik \\ |
48 \texttt{http://www.in.tum.de/\~\relax nipkow/}} |
48 \url{http://www.in.tum.de/~nipkow/}} |
49 \maketitle |
49 \maketitle |
50 |
50 |
51 \pagenumbering{roman} |
51 \pagenumbering{roman} |
52 \tableofcontents |
52 \tableofcontents |
53 |
53 |