# HG changeset patch
# User kuncar
# Date 1350568352 -7200
# Node ID e3f0a92de280ce0054be249d791b0a06954b4aca
# Parent  cde0a46b4224e4b08fa3e1598a846f394187e8dd
tuned proofs

diff -r cde0a46b4224 -r e3f0a92de280 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Thu Oct 18 15:52:31 2012 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Thu Oct 18 15:52:32 2012 +0200
@@ -140,18 +140,14 @@
 lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
 by (auto simp: not_Some_eq[THEN iffD1])
 
+lemma Set_set_keys: "Set x = dom (lookup x)" 
+by (auto simp: Set_def)
+
 lemma finite_Set [simp, intro!]: "finite (Set x)"
-proof -
-  have "Set x = dom (lookup x)" by (auto simp: Set_def)
-  then show ?thesis by simp
-qed
+by (simp add: Set_set_keys)
 
 lemma set_keys: "Set t = set(keys t)"
-proof -
- have "\<And>k. ((k, ()) \<in> set (entries t)) = (k \<in> set (keys t))" 
-    by (simp add: keys_entries)
-  then show ?thesis by (auto simp: lookup_in_tree Set_def)
-qed
+by (simp add: Set_set_keys lookup_keys)
 
 subsection {* fold and filter *}