src/HOL/Data_Structures/AA_Set.thy
changeset 63411 e051eea34990
parent 62526 347150095fd2
child 63636 6f38b7abb648
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Thu Jul 07 09:24:03 2016 +0200
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Thu Jul 07 18:08:02 2016 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  (*
     1.5 -Author: Tobias Nipkow and Daniel Stüwe
     1.6 +Author: Tobias Nipkow, Daniel Stüwe
     1.7  *)
     1.8  
     1.9  section \<open>AA Tree Implementation of Sets\<close>
    1.10 @@ -36,7 +36,7 @@
    1.11  
    1.12  hide_const (open) insert
    1.13  
    1.14 -fun insert :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.15 +fun insert :: "'a::linorder \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.16  "insert x Leaf = Node 1 Leaf x Leaf" |
    1.17  "insert x (Node lv t1 a t2) =
    1.18    (case cmp x a of
    1.19 @@ -81,7 +81,7 @@
    1.20  "del_max (Node lv l a Leaf) = (l,a)" |
    1.21  "del_max (Node lv l a r) = (let (r',b) = del_max r in (adjust(Node lv l a r'), b))"
    1.22  
    1.23 -fun delete :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.24 +fun delete :: "'a::linorder \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
    1.25  "delete _ Leaf = Leaf" |
    1.26  "delete x (Node lv l a r) =
    1.27    (case cmp x a of