1.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Mon Mar 05 15:47:11 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Wed Mar 07 15:54:11 2001 +0100
     1.3 @@ -1,17 +1,15 @@
     1.4  (*<*)
     1.5 -theory Nested2 = Nested0:;
     1.6 +theory Nested2 = Nested0:
     1.7  (*>*)
     1.8  
     1.9 -text{*\noindent
    1.10 -The termintion condition is easily proved by induction:
    1.11 -*};
    1.12 +text{*The termintion condition is easily proved by induction:*}
    1.13  
    1.14 -lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)";
    1.15 -by(induct_tac ts, auto);
    1.16 +lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)"
    1.17 +by(induct_tac ts, auto)
    1.18  (*<*)
    1.19  recdef trev "measure size"
    1.20   "trev (Var x) = Var x"
    1.21 - "trev (App f ts) = App f (rev(map trev ts))";
    1.22 + "trev (App f ts) = App f (rev(map trev ts))"
    1.23  (*>*)
    1.24  text{*\noindent
    1.25  By making this theorem a simplification rule, \isacommand{recdef}
    1.26 @@ -20,17 +18,16 @@
    1.27  lemma directly.  We no longer need the verbose
    1.28  induction schema for type @{text"term"} and can use the simpler one arising from
    1.29  @{term"trev"}:
    1.30 -*};
    1.31 +*}
    1.32  
    1.33 -lemma "trev(trev t) = t";
    1.34 -apply(induct_tac t rule:trev.induct);
    1.35 -txt{*\noindent
    1.36 -This leaves us with a trivial base case @{term"trev (trev (Var x)) = Var x"} and the step case
    1.37 -@{term[display,margin=60]"ALL t. t : set ts --> trev (trev t) = t ==> trev (trev (App f ts)) = App f ts"}
    1.38 -both of which are solved by simplification:
    1.39 -*};
    1.40 +lemma "trev(trev t) = t"
    1.41 +apply(induct_tac t rule:trev.induct)
    1.42 +txt{*
    1.43 +@{subgoals[display,indent=0]}
    1.44 +Both the base case and the induction step fall to simplification:
    1.45 +*}
    1.46  
    1.47 -by(simp_all add:rev_map sym[OF map_compose] cong:map_cong);
    1.48 +by(simp_all add:rev_map sym[OF map_compose] cong:map_cong)
    1.49  
    1.50  text{*\noindent
    1.51  If the proof of the induction step mystifies you, we recommend that you go through
    1.52 @@ -83,7 +80,7 @@
    1.53  by giving them the \isaindexbold{recdef_cong} attribute as in
    1.54  *}
    1.55  
    1.56 -declare map_cong[recdef_cong];
    1.57 +declare map_cong[recdef_cong]
    1.58  
    1.59  text{*
    1.60  Note that the @{text cong} and @{text recdef_cong} attributes are
    1.61 @@ -94,5 +91,5 @@
    1.62  %The simplifier's congruence rules cannot be used by recdef.
    1.63  %For example the weak congruence rules for if and case would prevent
    1.64  %recdef from generating sensible termination conditions.
    1.65 -*};
    1.66 -(*<*)end;(*>*)
    1.67 +*}
    1.68 +(*<*)end(*>*)