--- a/src/Doc/Tutorial/Misc/Tree.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/Tree.thy Sat Nov 01 14:20:38 2014 +0100
@@ -6,25 +6,25 @@
Define the datatype of \rmindex{binary trees}:
*}
-datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
+datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"(*<*)
primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
"mirror Tip = Tip" |
-"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
+"mirror (Node l x r) = Node (mirror r) x (mirror l)"(*>*)
text{*\noindent
Define a function @{term"mirror"} that mirrors a binary tree
by swapping subtrees recursively. Prove
*}
-lemma mirror_mirror: "mirror(mirror t) = t";
+lemma mirror_mirror: "mirror(mirror t) = t"
(*<*)
-apply(induct_tac t);
-by(auto);
+apply(induct_tac t)
+by(auto)
primrec flatten :: "'a tree => 'a list" where
"flatten Tip = []" |
-"flatten (Node l x r) = flatten l @ [x] @ flatten r";
+"flatten (Node l x r) = flatten l @ [x] @ flatten r"
(*>*)
text{*\noindent
@@ -32,10 +32,10 @@
by traversing it in infix order. Prove
*}
-lemma "flatten(mirror t) = rev(flatten t)";
+lemma "flatten(mirror t) = rev(flatten t)"
(*<*)
-apply(induct_tac t);
-by(auto);
+apply(induct_tac t)
+by(auto)
end
(*>*)