equal
deleted
inserted
replaced
1 \documentclass[11pt,a4paper]{article} |
1 \documentclass[envcountsame]{llncs} |
|
2 %\documentclass[11pt,a4paper]{article} |
2 \usepackage{isabelle,isabellesym,pdfsetup} |
3 \usepackage{isabelle,isabellesym,pdfsetup} |
3 |
4 |
4 %for best-style documents ... |
5 %for best-style documents ... |
5 \urlstyle{rm} |
6 \urlstyle{rm} |
6 %\isabellestyle{it} |
7 %\isabellestyle{it} |
7 |
8 |
8 \newtheorem{Exercise}{Exercise}[section] |
|
9 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}} |
|
10 |
|
11 \begin{document} |
9 \begin{document} |
12 |
10 |
13 \title{A Compact Introduction to Structured Proofs in Isar/HOL} |
11 \title{A Compact Introduction to Structured Proofs in Isar/HOL} |
14 \author{Tobias Nipkow\\Institut f{\"u}r Informatik, TU M{\"u}nchen\\ |
12 \author{Tobias Nipkow} |
|
13 \institute{Institut f{\"u}r Informatik, TU M{\"u}nchen\\ |
15 {\small\url{http://www.in.tum.de/~nipkow/}}} |
14 {\small\url{http://www.in.tum.de/~nipkow/}}} |
16 \date{} |
15 \date{} |
17 \maketitle |
16 \maketitle |
18 |
17 |
19 \begin{abstract} |
18 \begin{abstract} |