doc-src/TutorialI/Overview/document/root.tex
author kleing
Mon, 15 Oct 2001 21:04:32 +0200
changeset 11787 85b3735a51e1
parent 11238 1d789889c922
child 13238 a6cb18a25cbb
permissions -rw-r--r--
canonical 'cases'/'induct' rules for n-tuples (n=3..7) (really belongs to theory Product_Type, but doesn't work there yet)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11235
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
     2
\usepackage{isabelle,isabellesym,pdfsetup}
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
     3
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
     4
%for best-style documents ...
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
     5
\urlstyle{rm}
11238
1d789889c922 *** empty log message ***
nipkow
parents: 11235
diff changeset
     6
%\isabellestyle{it}
11235
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
     7
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
     8
\newtheorem{Exercise}{Exercise}[section]
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
     9
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
    10
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
    11
\begin{document}
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
    12
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
    13
\title{Overview}\maketitle
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
    14
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
    15
\input{session}
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
    16
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
    17
%\bibliographystyle{plain}
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
    18
%\bibliography{root}
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
    19
860c65c7388a *** empty log message ***
nipkow
parents:
diff changeset
    20
\end{document}