author nipkow Thu, 26 Oct 2000 10:27:04 +0200 changeset 10340 0a380ac80e7d parent 10339 ecb6eaa76843 child 10341 6eb91805a012
*** empty log message ***
 doc-src/TutorialI/todo.tobias file | annotate | diff | comparison | revisions doc-src/TutorialI/tutorial.tex file | annotate | diff | comparison | revisions
--- a/doc-src/TutorialI/todo.tobias	Thu Oct 26 09:15:59 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias	Thu Oct 26 10:27:04 2000 +0200
@@ -5,8 +5,6 @@
Why is comp needed in addition to op O?
Explain in syntax section!

-defs with = and pattern matching
-
replace "simp only split" by "split_tac".

arithmetic: allow mixed nat/int formulae
@@ -33,11 +31,17 @@
Induction rules for int: int_le/ge_induct?
Needed for ifak example. But is that example worth it?

+defs with = and pattern matching
+

Minor fixes in the tutorial
===========================

-explanation of absence of contrapos_pn in Rules?
+explanation of term "contrapositive"/contraposition in Rules?
+Index the notion and maybe the rules contrapos_xy
+
+Even: forward ref from problem with "Suc(Suc n) : even" to general solution in

get rid of use_thy in tutorial?

--- a/doc-src/TutorialI/tutorial.tex	Thu Oct 26 09:15:59 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Thu Oct 26 10:27:04 2000 +0200
@@ -58,10 +58,11 @@
\title{\includegraphics[scale=.8]{isabelle_hol}
\\ \vspace{0.5cm} The Tutorial
\\ --- DRAFT ---}
-\author{Tobias Nipkow\\
+\author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
Technische Universit{\"a}t M{\"u}nchen \\
-Institut f{\"u}r Informatik \\
-\url{http://www.in.tum.de/~nipkow/}}
+Institut f{\"u}r Informatik \\[1ex]
+University of Cambridge\\
+Computer Laboratory}
\maketitle

\pagenumbering{roman}
@@ -69,7 +70,7 @@

\subsubsection*{Acknowledgements}
This tutorial owes a lot to the constant discussions with and the valuable
-feedback from Larry Paulson and the Isabelle group at Munich: Olaf M{\"u}ller,
+feedback from the Isabelle group at Munich: Olaf M{\"u}ller,
Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
read and comment on a draft version.