changeset 70628 | 40b63f2655e8 |
parent 69597 | ff784d5a5bfb |
--- a/src/HOL/Data_Structures/Tree234_Set.thy Wed Aug 28 23:19:43 2019 +0200 +++ b/src/HOL/Data_Structures/Tree234_Set.thy Thu Aug 29 13:07:56 2019 +0200 @@ -208,7 +208,7 @@ subsubsection \<open>Functional correctness of isin:\<close> lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))" -by (induction t) (auto simp: isin_simps ball_Un) +by (induction t) (auto simp: isin_simps) subsubsection \<open>Functional correctness of insert:\<close>