Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Data_Structures/Tree23_Set.thy
changeset 70628 40b63f2655e8
parent 70274 7daa65d45462
child 72566 831f17da1aab 
--- 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"
isabelle