src/HOL/Data_Structures/AA_Map.thy
changeset 63411 e051eea34990
parent 62496 f187aaf602c4
child 67040 c1b87d15774a
     1.1 --- a/src/HOL/Data_Structures/AA_Map.thy	Thu Jul 07 09:24:03 2016 +0200
     1.2 +++ b/src/HOL/Data_Structures/AA_Map.thy	Thu Jul 07 18:08:02 2016 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4    Lookup2
     1.5  begin
     1.6  
     1.7 -fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
     1.8 +fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
     1.9  "update x y Leaf = Node 1 Leaf (x,y) Leaf" |
    1.10  "update x y (Node lv t1 (a,b) t2) =
    1.11    (case cmp x a of
    1.12 @@ -16,7 +16,7 @@
    1.13       GT \<Rightarrow> split (skew (Node lv t1 (a,b) (update x y t2))) |
    1.14       EQ \<Rightarrow> Node lv t1 (x,y) t2)"
    1.15  
    1.16 -fun delete :: "'a::cmp \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
    1.17 +fun delete :: "'a::linorder \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
    1.18  "delete _ Leaf = Leaf" |
    1.19  "delete x (Node lv l (a,b) r) =
    1.20    (case cmp x a of