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