changeset 32693 | 6c6b1ba5e71e |
parent 26933 | 7ca61b1ad872 |
child 32960 | 69916a850301 |
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Mon Sep 21 15:35:14 2009 +0200 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Mon Sep 21 15:35:15 2009 +0200 @@ -1747,7 +1747,7 @@ have "assigns (In1l e2) \<subseteq> dom (locals (store s2))" by (simp add: need_second_arg_def) with s2 - show ?thesis using False by (simp add: Un_subset_iff) + show ?thesis using False by simp qed next case Super thus ?case by simp