# HG changeset patch
# User nipkow
# Date 1042109140 -3600
# Node ID 23e743ac9cecabeb511215c7b8125a75b8b732bd
# Parent  f90298f884c4878b4048fb8a2f33bfbd9b73c2a1
*** empty log message ***

diff -r f90298f884c4 -r 23e743ac9cec doc-src/TutorialI/IsarOverview/Isar/Induction.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Induction.thy	Wed Jan 08 13:49:52 2003 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy	Thu Jan 09 11:45:40 2003 +0100
@@ -48,7 +48,6 @@
 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 (remember: $0-1=0$):
-%\Tweakskip
 *}
 (*<*)declare length_tl[simp del](*>*)
 lemma "length(tl xs) = length xs - 1"
@@ -286,8 +285,8 @@
 equation.
 
 The proof is so simple that it can be condensed to
-\Tweakskip
 *}
+
 (*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
 by (induct xs rule: rot.induct, simp_all)
 
diff -r f90298f884c4 -r 23e743ac9cec doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Jan 08 13:49:52 2003 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Thu Jan 09 11:45:40 2003 +0100
@@ -484,7 +484,6 @@
 @{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
 *}
 (*<*)ML"set quick_and_dirty"(*>*)
 lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"