fix duplicate simp rule warnings
authorhuffman
Sun Apr 25 23:22:29 2010 -0700 (2010-04-25)
changeset 363611debc8e29f6a
parent 36360 9d8f7efd9289
child 36362 06475a1547cb
fix duplicate simp rule warnings
src/HOL/Library/FrechetDeriv.thy
src/HOL/Library/Permutations.thy
     1.1 --- a/src/HOL/Library/FrechetDeriv.thy	Sun Apr 25 20:48:19 2010 -0700
     1.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Sun Apr 25 23:22:29 2010 -0700
     1.3 @@ -385,7 +385,7 @@
     1.4    fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
     1.5    shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
     1.6   apply (induct n)
     1.7 -  apply (simp add: power_Suc FDERIV_ident)
     1.8 +  apply (simp add: FDERIV_ident)
     1.9   apply (drule FDERIV_mult [OF FDERIV_ident])
    1.10   apply (simp only: of_nat_Suc left_distrib mult_1_left)
    1.11   apply (simp only: power_Suc right_distrib add_ac mult_ac)
     2.1 --- a/src/HOL/Library/Permutations.thy	Sun Apr 25 20:48:19 2010 -0700
     2.2 +++ b/src/HOL/Library/Permutations.thy	Sun Apr 25 23:22:29 2010 -0700
     2.3 @@ -96,7 +96,7 @@
     2.4  
     2.5  lemma permutes_superset:
     2.6    "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
     2.7 -by (simp add: Ball_def permutes_def Diff_iff) metis
     2.8 +by (simp add: Ball_def permutes_def) metis
     2.9  
    2.10  (* ------------------------------------------------------------------------- *)
    2.11  (* Group properties.                                                         *)
    2.12 @@ -125,7 +125,7 @@
    2.13    apply (rule permutes_compose[OF pS])
    2.14    apply (rule permutes_swap_id, simp)
    2.15    using permutes_in_image[OF pS, of a] apply simp
    2.16 -  apply (auto simp add: Ball_def Diff_iff swap_def)
    2.17 +  apply (auto simp add: Ball_def swap_def)
    2.18    done
    2.19  
    2.20  lemma permutes_insert: "{p. p permutes (insert a S)} =
    2.21 @@ -154,7 +154,7 @@
    2.22  lemma card_permutations: assumes Sn: "card S = n" and fS: "finite S"
    2.23    shows "card {p. p permutes S} = fact n"
    2.24  using fS Sn proof (induct arbitrary: n)
    2.25 -  case empty thus ?case by (simp add: permutes_empty)
    2.26 +  case empty thus ?case by simp
    2.27  next
    2.28    case (insert x F)
    2.29    { fix n assume H0: "card (insert x F) = n"