Merge

--- a/src/HOL/Filter.thy	Wed Sep 23 09:47:04 2015 +0200
+++ b/src/HOL/Filter.thy	Wed Sep 23 11:52:15 2015 +0100
@@ -994,7 +994,9 @@
 by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
 
 lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
-by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
+apply (simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
+apply (safe; metis)
+done
 
 lemma is_filter_parametric_aux:
   assumes "is_filter F"
@@ -1038,7 +1040,8 @@
 apply(rule iffI)
  apply(erule (3) is_filter_parametric_aux)
 apply(erule is_filter_parametric_aux[where A="conversep A"])
-apply(auto simp add: rel_fun_def)
+apply (simp_all add: rel_fun_def)
+apply metis
 done
 
 lemma left_total_rel_filter [transfer_rule]:

--- a/src/HOL/Int.thy	Wed Sep 23 09:47:04 2015 +0200
+++ b/src/HOL/Int.thy	Wed Sep 23 11:52:15 2015 +0100
@@ -258,6 +258,10 @@
   "0 = of_int z \<longleftrightarrow> z = 0"
   using of_int_eq_iff [of 0 z] by simp
 
+lemma of_int_eq_1_iff [iff]:
+   "of_int z = 1 \<longleftrightarrow> z = 1"
+  using of_int_eq_iff [of z 1] by simp
+
 end
 
 context linordered_idom
@@ -291,8 +295,49 @@
   "of_int z < 0 \<longleftrightarrow> z < 0"
   using of_int_less_iff [of z 0] by simp
 
+lemma of_int_1_le_iff [simp]:
+  "1 \<le> of_int z \<longleftrightarrow> 1 \<le> z"
+  using of_int_le_iff [of 1 z] by simp
+
+lemma of_int_le_1_iff [simp]:
+  "of_int z \<le> 1 \<longleftrightarrow> z \<le> 1"
+  using of_int_le_iff [of z 1] by simp
+
+lemma of_int_1_less_iff [simp]:
+  "1 < of_int z \<longleftrightarrow> 1 < z"
+  using of_int_less_iff [of 1 z] by simp
+
+lemma of_int_less_1_iff [simp]:
+  "of_int z < 1 \<longleftrightarrow> z < 1"
+  using of_int_less_iff [of z 1] by simp
+
 end
 
+text \<open>Comparisons involving @{term of_int}.\<close>
+
+lemma of_int_eq_numeral_iff [iff]:
+   "of_int z = (numeral n :: 'a::ring_char_0) 
+   \<longleftrightarrow> z = numeral n"
+  using of_int_eq_iff by fastforce
+
+lemma of_int_le_numeral_iff [simp]:           
+   "of_int z \<le> (numeral n :: 'a::linordered_idom) 
+   \<longleftrightarrow> z \<le> numeral n"
+  using of_int_le_iff [of z "numeral n"] by simp
+
+lemma of_int_numeral_le_iff [simp]:  
+   "(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z"
+  using of_int_le_iff [of "numeral n"] by simp
+
+lemma of_int_less_numeral_iff [simp]:           
+   "of_int z < (numeral n :: 'a::linordered_idom) 
+   \<longleftrightarrow> z < numeral n"
+  using of_int_less_iff [of z "numeral n"] by simp
+
+lemma of_int_numeral_less_iff [simp]:           
+   "(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z"
+  using of_int_less_iff [of "numeral n" z] by simp
+
 lemma of_nat_less_of_int_iff:
   "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
   by (metis of_int_of_nat_eq of_int_less_iff)

--- a/src/HOL/MicroJava/DFA/Product.thy	Wed Sep 23 09:47:04 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Product.thy	Wed Sep 23 11:52:15 2015 +0100
@@ -43,7 +43,7 @@
   "order(Product.le rA rB) = (order rA & order rB)"
 apply (unfold Semilat.order_def)
 apply simp
-apply blast
+apply meson
 done 
 
 lemma acc_le_prodI [intro!]:

--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Sep 23 09:47:04 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Sep 23 11:52:15 2015 +0100
@@ -501,10 +501,10 @@
   unfolding holomorphic_on_def by (metis complex_differentiable_setsum)
 
 definition deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "deriv f x \<equiv> THE D. DERIV f x :> D"
+  "deriv f x \<equiv> SOME D. DERIV f x :> D"
 
 lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
-  unfolding deriv_def by (metis the_equality DERIV_unique)
+  unfolding deriv_def by (metis some_equality DERIV_unique)
 
 lemma DERIV_deriv_iff_real_differentiable:
   fixes x :: real

--- a/src/HOL/Topological_Spaces.thy	Wed Sep 23 09:47:04 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed Sep 23 11:52:15 2015 +0100
@@ -377,6 +377,10 @@
 lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
   unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
 
+lemma at_within_open_NO_MATCH:
+  "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
+  by (simp only: at_within_open)
+
 lemma at_within_empty [simp]: "at a within {} = bot"
   unfolding at_within_def by simp