src/HOL/UNITY/Transformers.thy
changeset 44106 0e018cbcc0de
parent 37936 1e4c5015a72e
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Tue Aug 09 18:52:18 2011 +0200
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Tue Aug 09 20:24:48 2011 +0200
     1.3 @@ -467,7 +467,7 @@
     1.4        "single_valued act
     1.5         ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> 
     1.6             wens_set (mk_program (init, {act}, allowed)) B"
     1.7 -apply (simp add: wens_single_eq_Union UN_eq) 
     1.8 +apply (simp add: SUP_def image_def wens_single_eq_Union) 
     1.9  apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
    1.10  done
    1.11