# HG changeset patch
# User nipkow
# Date 1041199959 -3600
# Node ID 1764a81b7a0a983bcdd6fffdc0a4f1c29364067c
# Parent  731171c27be9ac904153f11153e56bbb9aea79e4
*** empty log message ***

diff -r 731171c27be9 -r 1764a81b7a0a doc-src/TutorialI/IsarOverview/Isar/Induction.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Induction.thy	Sun Dec 29 18:31:31 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy	Sun Dec 29 23:12:39 2002 +0100
@@ -48,7 +48,7 @@
 The same game can be played with other datatypes, for example lists,
 where @{term tl} is the tail of a list, and @{text length} returns a
 natural number:
-\Tweakskip
+%\Tweakskip
 *}
 (*<*)declare length_tl[simp del](*>*)
 lemma "length(tl xs) = length xs - 1"
@@ -286,7 +286,8 @@
 equation.
 
 The proof is so simple that it can be condensed to
-\Tweakskip*}
+%\Tweakskip
+*}
 (*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
 by (induct xs rule: rot.induct, simp_all)
 
diff -r 731171c27be9 -r 1764a81b7a0a doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Sun Dec 29 18:31:31 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Sun Dec 29 23:12:39 2002 +0100
@@ -479,7 +479,7 @@
 @{text blast} to achieve bigger proof steps, there may still be the
 tendency to use the default introduction and elimination rules to
 decompose goals and facts. This can lead to very tedious proofs:
-\Tweakskip
+%\Tweakskip
 *}
 (*<*)ML"set quick_and_dirty"(*>*)
 lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"
diff -r 731171c27be9 -r 1764a81b7a0a doc-src/TutorialI/IsarOverview/Isar/document/root.bib
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.bib	Sun Dec 29 18:31:31 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.bib	Sun Dec 29 23:12:39 2002 +0100
@@ -1,5 +1,6 @@
 @string{LNCS="Lect.\ Notes in Comp.\ Sci."}
 @string{Springer="Springer-Verlag"}
+@string{JAR="J. Automated Reasoning"}
 
 @InProceedings{BauerW-TPHOLs01,
 author={Gertrud Bauer and Markus Wenzel},
@@ -45,6 +46,7 @@
 year=2002,
 note={\url{http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html}}}
 
-@unpublished{WenzelW-JAR,author={Markus Wenzel and Freek Wiedijk},
+@article{WenzelW-JAR,author={Markus Wenzel and Freek Wiedijk},
 title={A comparison of the mathematical proof languages {Mizar} and {Isar}},
-note={Submitted for publication},year=2002}
+journal=JAR,year=2003,note={To appear}}
+
diff -r 731171c27be9 -r 1764a81b7a0a doc-src/TutorialI/IsarOverview/Isar/document/root.tex
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Sun Dec 29 18:31:31 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Sun Dec 29 23:12:39 2002 +0100
@@ -32,10 +32,10 @@
 
 \input{intro.tex}
 \input{Logic.tex}
-\Tweakskip\Tweakskip
+%\Tweakskip\Tweakskip
 \input{Induction.tex}
 
-\Tweakskip
+%\Tweakskip
 \small
 \paragraph{Acknowledgement}
 I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,