summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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)