*** empty log message ***
authornipkow
Thu Oct 26 10:27:04 2000 +0200 (2000-10-26)
changeset 103400a380ac80e7d
parent 10339 ecb6eaa76843
child 10341 6eb91805a012
*** empty log message ***
doc-src/TutorialI/todo.tobias
doc-src/TutorialI/tutorial.tex
     1.1 --- a/doc-src/TutorialI/todo.tobias	Thu Oct 26 09:15:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/todo.tobias	Thu Oct 26 10:27:04 2000 +0200
     1.3 @@ -5,8 +5,6 @@
     1.4  Why is comp needed in addition to op O?
     1.5  Explain in syntax section!
     1.6  
     1.7 -defs with = and pattern matching
     1.8 -
     1.9  replace "simp only split" by "split_tac".
    1.10  
    1.11  arithmetic: allow mixed nat/int formulae
    1.12 @@ -33,11 +31,17 @@
    1.13  Induction rules for int: int_le/ge_induct?
    1.14  Needed for ifak example. But is that example worth it?
    1.15  
    1.16 +defs with = and pattern matching
    1.17 +
    1.18  
    1.19  Minor fixes in the tutorial
    1.20  ===========================
    1.21  
    1.22 -explanation of absence of contrapos_pn in Rules?
    1.23 +explanation of term "contrapositive"/contraposition in Rules?
    1.24 +Index the notion and maybe the rules contrapos_xy
    1.25 +
    1.26 +Even: forward ref from problem with "Suc(Suc n) : even" to general solution in
    1.27 +AdvancedInd section.
    1.28  
    1.29  get rid of use_thy in tutorial?
    1.30  
     2.1 --- a/doc-src/TutorialI/tutorial.tex	Thu Oct 26 09:15:59 2000 +0200
     2.2 +++ b/doc-src/TutorialI/tutorial.tex	Thu Oct 26 10:27:04 2000 +0200
     2.3 @@ -58,10 +58,11 @@
     2.4  \title{\includegraphics[scale=.8]{isabelle_hol}
     2.5         \\ \vspace{0.5cm} The Tutorial
     2.6         \\ --- DRAFT ---}
     2.7 -\author{Tobias Nipkow\\
     2.8 +\author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
     2.9  Technische Universit{\"a}t M{\"u}nchen \\
    2.10 -Institut f{\"u}r Informatik \\
    2.11 -\url{http://www.in.tum.de/~nipkow/}}
    2.12 +Institut f{\"u}r Informatik \\[1ex]
    2.13 +University of Cambridge\\
    2.14 +Computer Laboratory}
    2.15  \maketitle
    2.16  
    2.17  \pagenumbering{roman}
    2.18 @@ -69,7 +70,7 @@
    2.19  
    2.20  \subsubsection*{Acknowledgements}
    2.21  This tutorial owes a lot to the constant discussions with and the valuable
    2.22 -feedback from Larry Paulson and the Isabelle group at Munich: Olaf M{\"u}ller,
    2.23 +feedback from the Isabelle group at Munich: Olaf M{\"u}ller,
    2.24  Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
    2.25  and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
    2.26  read and comment on a draft version.