# HG changeset patch
# User huffman
# Date 1272262949 25200
# Node ID 1debc8e29f6a7f58f7e461fa1f46f2a1db7a93a6
# Parent  9d8f7efd928991bfbd698daa2c78dcba047f7902
fix duplicate simp rule warnings

diff -r 9d8f7efd9289 -r 1debc8e29f6a src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Sun Apr 25 20:48:19 2010 -0700
+++ b/src/HOL/Library/FrechetDeriv.thy	Sun Apr 25 23:22:29 2010 -0700
@@ -385,7 +385,7 @@
   fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
   shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
  apply (induct n)
-  apply (simp add: power_Suc FDERIV_ident)
+  apply (simp add: FDERIV_ident)
  apply (drule FDERIV_mult [OF FDERIV_ident])
  apply (simp only: of_nat_Suc left_distrib mult_1_left)
  apply (simp only: power_Suc right_distrib add_ac mult_ac)
diff -r 9d8f7efd9289 -r 1debc8e29f6a src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Sun Apr 25 20:48:19 2010 -0700
+++ b/src/HOL/Library/Permutations.thy	Sun Apr 25 23:22:29 2010 -0700
@@ -96,7 +96,7 @@
 
 lemma permutes_superset:
   "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
-by (simp add: Ball_def permutes_def Diff_iff) metis
+by (simp add: Ball_def permutes_def) metis
 
 (* ------------------------------------------------------------------------- *)
 (* Group properties.                                                         *)
@@ -125,7 +125,7 @@
   apply (rule permutes_compose[OF pS])
   apply (rule permutes_swap_id, simp)
   using permutes_in_image[OF pS, of a] apply simp
-  apply (auto simp add: Ball_def Diff_iff swap_def)
+  apply (auto simp add: Ball_def swap_def)
   done
 
 lemma permutes_insert: "{p. p permutes (insert a S)} =
@@ -154,7 +154,7 @@
 lemma card_permutations: assumes Sn: "card S = n" and fS: "finite S"
   shows "card {p. p permutes S} = fact n"
 using fS Sn proof (induct arbitrary: n)
-  case empty thus ?case by (simp add: permutes_empty)
+  case empty thus ?case by simp
 next
   case (insert x F)
   { fix n assume H0: "card (insert x F) = n"