src/Doc/Tutorial/Misc/Itrev.thy
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 67406 23307fd33906
     1.1 --- a/src/Doc/Tutorial/Misc/Itrev.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Tutorial/Misc/Itrev.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -58,15 +58,15 @@
     1.4  
     1.5  Naturally, we would like to show that @{term"itrev"} does indeed reverse
     1.6  its first argument provided the second one is empty:
     1.7 -*};
     1.8 +*}
     1.9  
    1.10 -lemma "itrev xs [] = rev xs";
    1.11 +lemma "itrev xs [] = rev xs"
    1.12  
    1.13  txt{*\noindent
    1.14  There is no choice as to the induction variable, and we immediately simplify:
    1.15 -*};
    1.16 +*}
    1.17  
    1.18 -apply(induct_tac xs, simp_all);
    1.19 +apply(induct_tac xs, simp_all)
    1.20  
    1.21  txt{*\noindent
    1.22  Unfortunately, this attempt does not prove
    1.23 @@ -80,9 +80,9 @@
    1.24  \end{quote}
    1.25  Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
    1.26  just not true.  The correct generalization is
    1.27 -*};
    1.28 -(*<*)oops;(*>*)
    1.29 -lemma "itrev xs ys = rev xs @ ys";
    1.30 +*}
    1.31 +(*<*)oops(*>*)
    1.32 +lemma "itrev xs ys = rev xs @ ys"
    1.33  (*<*)apply(induct_tac xs, simp_all)(*>*)
    1.34  txt{*\noindent
    1.35  If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
    1.36 @@ -100,11 +100,11 @@
    1.37  the subgoal, but the induction hypothesis needs to be applied with
    1.38  @{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem
    1.39  for all @{term"ys"} instead of a fixed one:
    1.40 -*};
    1.41 -(*<*)oops;(*>*)
    1.42 -lemma "\<forall>ys. itrev xs ys = rev xs @ ys";
    1.43 +*}
    1.44 +(*<*)oops(*>*)
    1.45 +lemma "\<forall>ys. itrev xs ys = rev xs @ ys"
    1.46  (*<*)
    1.47 -by(induct_tac xs, simp_all);
    1.48 +by(induct_tac xs, simp_all)
    1.49  (*>*)
    1.50  
    1.51  text{*\noindent