# HG changeset patch
# User krauss
# Date 1262165093 -3600
# Node ID c7f621786035d5521ef16f0bc5ce99bc55c84268
# Parent  a7acd6c68d9b8b107206130fef545b0fe2f8a946
killed a few warnings

diff -r a7acd6c68d9b -r c7f621786035 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Dec 30 01:08:33 2009 +0100
+++ b/src/HOL/Fun.thy	Wed Dec 30 10:24:53 2009 +0100
@@ -171,7 +171,7 @@
 by (simp add: surj_def) 
 
 lemma bij_id[simp]: "bij id"
-by (simp add: bij_def inj_on_id surj_id) 
+by (simp add: bij_def)
 
 lemma inj_onI:
     "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A"
@@ -432,14 +432,14 @@
 by (rule ext, auto)
 
 lemma inj_on_fun_updI: "\<lbrakk> inj_on f A; y \<notin> f`A \<rbrakk> \<Longrightarrow> inj_on (f(x:=y)) A"
-by(fastsimp simp:inj_on_def image_def)
+by (fastsimp simp:inj_on_def image_def)
 
 lemma fun_upd_image:
      "f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
 by auto
 
 lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
-by(auto intro: ext)
+by (auto intro: ext)
 
 
 subsection {* @{text override_on} *}
@@ -496,7 +496,7 @@
   thus "inj_on f A" by simp 
 next
   assume "inj_on f A"
-  with A show "inj_on (swap a b f) A" by(iprover intro: inj_on_imp_inj_on_swap)
+  with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
 qed
 
 lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
@@ -529,7 +529,7 @@
 lemma the_inv_into_f_f:
   "[| inj_on f A;  x : A |] ==> the_inv_into A f (f x) = x"
 apply (simp add: the_inv_into_def inj_on_def)
-apply (blast intro: the_equality)
+apply blast
 done
 
 lemma f_the_inv_into_f:
diff -r a7acd6c68d9b -r c7f621786035 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Dec 30 01:08:33 2009 +0100
+++ b/src/HOL/HOL.thy	Wed Dec 30 10:24:53 2009 +0100
@@ -869,7 +869,6 @@
   and impCE [elim!]
   and disjE [elim!]
   and conjE [elim!]
-  and conjE [elim!]
 
 declare ex_ex1I [intro!]
   and allI [intro!]
diff -r a7acd6c68d9b -r c7f621786035 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Dec 30 01:08:33 2009 +0100
+++ b/src/HOL/Lattices.thy	Wed Dec 30 10:24:53 2009 +0100
@@ -201,7 +201,7 @@
 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
 proof-
   have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
-  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc del:sup_absorb1)
+  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
   also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
     by(simp add:inf_sup_absorb inf_commute)
   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
@@ -213,7 +213,7 @@
 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
 proof-
   have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
-  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc del:inf_absorb1)
+  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
   also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
     by(simp add:sup_inf_absorb sup_commute)
   also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
@@ -404,7 +404,7 @@
     by (simp add: inf_sup_distrib1)
   then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"
     using sup_compl_top assms(2) by simp
-  then show "- x = y" by (simp add: inf_top_right)
+  then show "- x = y" by simp
 qed
 
 lemma double_compl [simp]:
diff -r a7acd6c68d9b -r c7f621786035 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Dec 30 01:08:33 2009 +0100
+++ b/src/HOL/Set.thy	Wed Dec 30 10:24:53 2009 +0100
@@ -517,10 +517,10 @@
 *}
 
 lemma equalityD1: "A = B ==> A \<subseteq> B"
-  by (simp add: subset_refl)
+  by simp
 
 lemma equalityD2: "A = B ==> B \<subseteq> A"
-  by (simp add: subset_refl)
+  by simp
 
 text {*
   \medskip Be careful when adding this to the claset as @{text
@@ -529,7 +529,7 @@
 *}
 
 lemma equalityE: "A = B ==> (A \<subseteq> B ==> B \<subseteq> A ==> P) ==> P"
-  by (simp add: subset_refl)
+  by simp
 
 lemma equalityCE [elim]:
     "A = B ==> (c \<in> A ==> c \<in> B ==> P) ==> (c \<notin> A ==> c \<notin> B ==> P) ==> P"
@@ -629,7 +629,7 @@
   by simp
 
 lemma Pow_top: "A \<in> Pow A"
-  by (simp add: subset_refl)
+  by simp
 
 
 subsubsection {* Set complement *}