src/HOL/Library/Multiset.thy
changeset 59807 22bc39064290
parent 59625 aacdce52b2fc
child 59813 6320064f22bb
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Mar 25 10:41:53 2015 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Mar 25 10:44:57 2015 +0100
     1.3 @@ -1658,7 +1658,7 @@
     1.4   apply (simp (no_asm))
     1.5   apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
     1.6   apply (simp (no_asm_simp) add: add.assoc [symmetric])
     1.7 - apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong)
     1.8 + apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong)
     1.9   apply (simp add: diff_union_single_conv)
    1.10   apply (simp (no_asm_use) add: trans_def)
    1.11   apply blast
    1.12 @@ -1669,7 +1669,7 @@
    1.13   apply (rule conjI)
    1.14    apply (simp add: multiset_eq_iff split: nat_diff_split)
    1.15   apply (rule conjI)
    1.16 -  apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong, simp)
    1.17 +  apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong, simp)
    1.18    apply (simp add: multiset_eq_iff split: nat_diff_split)
    1.19   apply (simp (no_asm_use) add: trans_def)
    1.20   apply blast
    1.21 @@ -1692,7 +1692,7 @@
    1.22   apply (simp add: mult1_def set_of_def, blast)
    1.23  txt {* Now we know @{term "J' \<noteq> {#}"}. *}
    1.24  apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
    1.25 -apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
    1.26 +apply (erule_tac P = "\<forall>k \<in> set_of K. P k" for P in rev_mp)
    1.27  apply (erule ssubst)
    1.28  apply (simp add: Ball_def, auto)
    1.29  apply (subgoal_tac