src/HOL/UNITY/Transformers.thy
changeset 59807 22bc39064290
parent 58889 5b7a9633cfa8
child 62343 24106dc44def
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Wed Mar 25 10:41:53 2015 +0100
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Wed Mar 25 10:44:57 2015 +0100
     1.3 @@ -139,7 +139,7 @@
     1.4        "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
     1.5         ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
     1.6  apply (rule subset_wens) 
     1.7 -apply (rule_tac P="\<lambda>x. ?f x \<subseteq> ?b" in ssubst [OF wens_unfold])
     1.8 +apply (rule_tac P="\<lambda>x. f x \<subseteq> b" for f b in ssubst [OF wens_unfold])
     1.9  apply (simp add: wp_def awp_def, blast)
    1.10  done
    1.11