merged
authornipkow
Wed Jan 13 09:38:24 2016 +0100 (2016-01-13 ago)
changeset 621619aa4012fc45d
parent 62159 56d35d0fda5b
parent 62160 ff20b44b2fc8
child 62162 dca35981c8fb
merged
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Wed Jan 13 09:09:38 2016 +0100
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Wed Jan 13 09:38:24 2016 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4      else
     1.5        case r of
     1.6          Leaf \<Rightarrow> Leaf (* unreachable *) |
     1.7 -        Node _ t1 b t4 \<Rightarrow>
     1.8 +        Node lvb t1 b t4 \<Rightarrow>
     1.9            (case t1 of
    1.10               Node lva t2 a t3
    1.11                 \<Rightarrow> Node (lva+1) (Node (lv-1) l x t2) a
     2.1 --- a/src/HOL/Data_Structures/Tree2.thy	Wed Jan 13 09:09:38 2016 +0100
     2.2 +++ b/src/HOL/Data_Structures/Tree2.thy	Wed Jan 13 09:38:24 2016 +0100
     2.3 @@ -4,7 +4,7 @@
     2.4  
     2.5  datatype ('a,'b) tree =
     2.6    Leaf ("\<langle>\<rangle>") |
     2.7 -  Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("\<langle>_, _, _, _\<rangle>")
     2.8 +  Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("(1\<langle>_,/ _,/ _,/ _\<rangle>)")
     2.9  
    2.10  fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where
    2.11  "inorder Leaf = []" |
     3.1 --- a/src/HOL/Library/Tree.thy	Wed Jan 13 09:09:38 2016 +0100
     3.2 +++ b/src/HOL/Library/Tree.thy	Wed Jan 13 09:38:24 2016 +0100
     3.3 @@ -7,8 +7,8 @@
     3.4  begin
     3.5  
     3.6  datatype 'a tree =
     3.7 -  Leaf ("\<langle>\<rangle>") |
     3.8 -  Node (left: "'a tree") (val: 'a) (right: "'a tree") ("\<langle>_, _, _\<rangle>")
     3.9 +  is_Leaf: Leaf ("\<langle>\<rangle>") |
    3.10 +  Node (left: "'a tree") (val: 'a) (right: "'a tree") ("(1\<langle>_,/ _,/ _\<rangle>)")
    3.11    where
    3.12      "left Leaf = Leaf"
    3.13    | "right Leaf = Leaf"