src/HOL/ex/Execute_Choice.thy
changeset 44174 d1d79f0e1ea6
parent 41413 64cd30d6b0b8
child 44899 95a53c01ed61
--- a/src/HOL/ex/Execute_Choice.thy	Fri Aug 12 09:17:30 2011 -0700
+++ b/src/HOL/ex/Execute_Choice.thy	Fri Aug 12 14:45:50 2011 -0700
@@ -26,7 +26,7 @@
   case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def)
 next
   case False
-  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def fun_eq_iff mem_def keys_def)
+  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def keys_def)
   then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
      the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
        (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"