src/HOL/UNITY/Transformers.thy
changeset 46911 6d2a2f0e904e
parent 44890 22f665a2e91c
child 56248 67dc9549fa15
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Tue Mar 13 21:17:37 2012 +0100
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Tue Mar 13 22:49:02 2012 +0100
     1.3 @@ -422,7 +422,7 @@
     1.4          W \<subseteq> insert (wens_single act B)
     1.5              (range (wens_single_finite act B))\<rbrakk>
     1.6         \<Longrightarrow> \<Union>W = wens_single act B"
     1.7 -apply (case_tac "wens_single act B \<in> W")
     1.8 +apply (cases "wens_single act B \<in> W")
     1.9   apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD]) 
    1.10  apply (simp add: wens_single_eq_Union) 
    1.11  apply (rule equalityI, blast)