src/HOL/Library/Permutations.thy
 changeset 36361 1debc8e29f6a parent 36335 ceea7e15c04b child 39198 f967a16dfcdd
```     1.1 --- a/src/HOL/Library/Permutations.thy	Sun Apr 25 20:48:19 2010 -0700
1.2 +++ b/src/HOL/Library/Permutations.thy	Sun Apr 25 23:22:29 2010 -0700
1.3 @@ -96,7 +96,7 @@
1.4
1.5  lemma permutes_superset:
1.6    "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
1.7 -by (simp add: Ball_def permutes_def Diff_iff) metis
1.8 +by (simp add: Ball_def permutes_def) metis
1.9
1.10  (* ------------------------------------------------------------------------- *)
1.11  (* Group properties.                                                         *)
1.12 @@ -125,7 +125,7 @@
1.13    apply (rule permutes_compose[OF pS])
1.14    apply (rule permutes_swap_id, simp)
1.15    using permutes_in_image[OF pS, of a] apply simp
1.16 -  apply (auto simp add: Ball_def Diff_iff swap_def)
1.17 +  apply (auto simp add: Ball_def swap_def)
1.18    done
1.19
1.20  lemma permutes_insert: "{p. p permutes (insert a S)} =
1.21 @@ -154,7 +154,7 @@
1.22  lemma card_permutations: assumes Sn: "card S = n" and fS: "finite S"
1.23    shows "card {p. p permutes S} = fact n"
1.24  using fS Sn proof (induct arbitrary: n)
1.25 -  case empty thus ?case by (simp add: permutes_empty)
1.26 +  case empty thus ?case by simp
1.27  next
1.28    case (insert x F)
1.29    { fix n assume H0: "card (insert x F) = n"
```