changeset 14398 | c5c47703f763 |
parent 14030 | cd928c0ac225 |
child 16417 | 9bc16273c2d4 |
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Feb 19 15:57:34 2004 +0100 @@ -3429,7 +3429,7 @@ by (cases s2) (simp add: abrupt_if_def) with brkAss_C1 s1_s2 s2_s3 show ?thesis - by simp (blast intro: subset_trans) + by simp qed moreover from True nrmAss_C2 s2_s3 have "nrm C2 \<subseteq> dom (locals (store s3))"