changeset 62343 | 24106dc44def |
parent 59807 | 22bc39064290 |
child 63146 | f1ecba0272f9 |
--- a/src/HOL/UNITY/Transformers.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/UNITY/Transformers.thy Wed Feb 17 21:51:56 2016 +0100 @@ -467,7 +467,7 @@ "single_valued act ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> wens_set (mk_program (init, {act}, allowed)) B" -apply (simp add: SUP_def image_def wens_single_eq_Union) +apply (simp add: image_def wens_single_eq_Union) apply (blast intro: wens_set.Union wens_single_finite_in_wens_set) done