# 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 \ [] \ 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 "\x y. A x y \ B x y \ C x y"