# HG changeset patch
# User nipkow
# Date 1567076876 -7200
# Node ID 40b63f2655e8c27523c35c3c85edf61c3e28d585
# Parent  e59a4ae35b888f41dfe9520a5b59d2694024b775
tuned proof

diff -r e59a4ae35b88 -r 40b63f2655e8 src/HOL/Data_Structures/Tree234_Set.thy
--- 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>
diff -r e59a4ae35b88 -r 40b63f2655e8 src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Wed Aug 28 23:19:43 2019 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Thu Aug 29 13:07:56 2019 +0200
@@ -148,7 +148,7 @@
 subsubsection "Proofs for isin"
 
 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 "Proofs for insert"