--- a/src/Doc/Tutorial/Misc/Tree.thy Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Misc/Tree.thy Fri Jan 12 14:08:53 2018 +0100
@@ -2,9 +2,9 @@
theory Tree imports Main begin
(*>*)
-text{*\noindent
+text\<open>\noindent
Define the datatype of \rmindex{binary trees}:
-*}
+\<close>
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"(*<*)
@@ -12,10 +12,10 @@
"mirror Tip = Tip" |
"mirror (Node l x r) = Node (mirror r) x (mirror l)"(*>*)
-text{*\noindent
+text\<open>\noindent
Define a function @{term"mirror"} that mirrors a binary tree
by swapping subtrees recursively. Prove
-*}
+\<close>
lemma mirror_mirror: "mirror(mirror t) = t"
(*<*)
@@ -27,10 +27,10 @@
"flatten (Node l x r) = flatten l @ [x] @ flatten r"
(*>*)
-text{*\noindent
+text\<open>\noindent
Define a function @{term"flatten"} that flattens a tree into a list
by traversing it in infix order. Prove
-*}
+\<close>
lemma "flatten(mirror t) = rev(flatten t)"
(*<*)