--- a/src/HOL/Data_Structures/AA_Set.thy Wed Jan 13 09:09:38 2016 +0100
+++ b/src/HOL/Data_Structures/AA_Set.thy Wed Jan 13 09:38:24 2016 +0100
@@ -72,7 +72,7 @@
else
case r of
Leaf \<Rightarrow> Leaf (* unreachable *) |
- Node _ t1 b t4 \<Rightarrow>
+ Node lvb t1 b t4 \<Rightarrow>
(case t1 of
Node lva t2 a t3
\<Rightarrow> Node (lva+1) (Node (lv-1) l x t2) a
--- a/src/HOL/Data_Structures/Tree2.thy Wed Jan 13 09:09:38 2016 +0100
+++ b/src/HOL/Data_Structures/Tree2.thy Wed Jan 13 09:38:24 2016 +0100
@@ -4,7 +4,7 @@
datatype ('a,'b) tree =
Leaf ("\<langle>\<rangle>") |
- Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("\<langle>_, _, _, _\<rangle>")
+ Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("(1\<langle>_,/ _,/ _,/ _\<rangle>)")
fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where
"inorder Leaf = []" |
--- a/src/HOL/Library/Tree.thy Wed Jan 13 09:09:38 2016 +0100
+++ b/src/HOL/Library/Tree.thy Wed Jan 13 09:38:24 2016 +0100
@@ -7,8 +7,8 @@
begin
datatype 'a tree =
- Leaf ("\<langle>\<rangle>") |
- Node (left: "'a tree") (val: 'a) (right: "'a tree") ("\<langle>_, _, _\<rangle>")
+ is_Leaf: Leaf ("\<langle>\<rangle>") |
+ Node (left: "'a tree") (val: 'a) (right: "'a tree") ("(1\<langle>_,/ _,/ _\<rangle>)")
where
"left Leaf = Leaf"
| "right Leaf = Leaf"