| changeset 63412 | def97df48390 |
| parent 63411 | e051eea34990 |
| child 67929 | 30486b96274d |
--- a/src/HOL/Data_Structures/Isin2.thy Thu Jul 07 17:34:39 2016 +0200 +++ b/src/HOL/Data_Structures/Isin2.thy Thu Jul 07 18:08:10 2016 +0200 @@ -9,7 +9,7 @@ Set_by_Ordered begin -fun isin :: "('a::cmp,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where +fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where "isin Leaf x = False" | "isin (Node _ l a r) x = (case cmp x a of