changeset 63649 | e690d6f2185b |
parent 63310 | caaacf37943f |
child 64587 | 8355a6e2df79 |
--- a/src/HOL/Library/Permutation.thy Wed Aug 10 09:33:54 2016 +0200 +++ b/src/HOL/Library/Permutation.thy Wed Aug 10 14:50:59 2016 +0200 @@ -95,7 +95,7 @@ by auto proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys" - by (drule_tac z = z in perm_remove_perm) auto + by (drule perm_remove_perm [where z = z]) auto proposition cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys" by (blast intro: cons_perm_imp_perm)