doc-src/TutorialI/Misc/Tree2.thy

--- a/doc-src/TutorialI/Misc/Tree2.thy	Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/Tree2.thy	Thu May 29 22:45:33 2008 +0200
@@ -6,25 +6,21 @@
 @{term"flatten"} from trees to lists. The straightforward version of
 @{term"flatten"} is based on @{text"@"} and is thus, like @{term"rev"},
 quadratic. A linear time version of @{term"flatten"} again reqires an extra
-argument, the accumulator: *}
-
-consts flatten2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list"
-(*<*)
-primrec
-"flatten2 Tip xs = xs"
+argument, the accumulator. Define *}
+(*<*)primrec(*>*)flatten2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list"(*<*)where
+"flatten2 Tip xs = xs" |
 "flatten2 (Node l x r) xs = flatten2 l (x#(flatten2 r xs))"
 (*>*)
 
-text{*\noindent Define @{term"flatten2"} and prove
-*}
+text{*\noindent and prove*}
 (*<*)
-lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs";
-apply(induct_tac t);
+lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs"
+apply(induct_tac t)
 by(auto);
 (*>*)
-lemma "flatten2 t [] = flatten t";
+lemma "flatten2 t [] = flatten t"
 (*<*)
-by(simp);
+by(simp)
 
 end
 (*>*)