--- a/NEWS Mon Sep 05 23:11:00 2016 +0200
+++ b/NEWS Mon Sep 05 23:39:15 2016 +0200
@@ -334,8 +334,12 @@
INCOMPATIBILITY.
- The "size" plugin has been made compatible again with locales.
-* Removed obsolete theorem nat_less_cases. INCOMPATIBILITY, use
-linorder_cases instead.
+* Some old / obsolete theorems have been renamed / removed, potential
+INCOMPATIBILITY.
+
+ nat_less_cases -- removed, use linorder_cases instead
+ inv_image_comp -- removed, use image_inv_f_f instead
+ image_surj_f_inv_f ~> image_f_inv_f
* Some theorems about groups and orders have been generalised from
groups to semi-groups that are also monoids:
--- a/src/HOL/Analysis/Polytope.thy Mon Sep 05 23:11:00 2016 +0200
+++ b/src/HOL/Analysis/Polytope.thy Mon Sep 05 23:39:15 2016 +0200
@@ -2386,7 +2386,7 @@
have *: "{f. P f} = (image h) ` {f. P (h ` f)}" for P
apply safe
apply (rule_tac x="inv h ` x" in image_eqI)
- apply (auto simp: \<open>bij h\<close> bij_is_surj image_surj_f_inv_f)
+ apply (auto simp: \<open>bij h\<close> bij_is_surj image_f_inv_f)
done
have "inj h" using bij_is_inj assms by blast
then have injim: "inj_on (op ` h) A" for A
--- a/src/HOL/Hilbert_Choice.thy Mon Sep 05 23:11:00 2016 +0200
+++ b/src/HOL/Hilbert_Choice.thy Mon Sep 05 23:39:15 2016 +0200
@@ -244,15 +244,12 @@
lemma o_inv_distrib: "bij f \<Longrightarrow> bij g \<Longrightarrow> inv (f \<circ> g) = inv g \<circ> inv f"
by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)
-lemma image_surj_f_inv_f: "surj f \<Longrightarrow> f ` (inv f ` A) = A"
+lemma image_f_inv_f: "surj f \<Longrightarrow> f ` (inv f ` A) = A"
by (simp add: surj_f_inv_f image_comp comp_def)
lemma image_inv_f_f: "inj f \<Longrightarrow> inv f ` (f ` A) = A"
by simp
-lemma inv_image_comp: "inj f \<Longrightarrow> inv f ` (f ` X) = X"
- by (fact image_inv_f_f)
-
lemma bij_image_Collect_eq: "bij f \<Longrightarrow> f ` Collect P = {y. P (inv f y)}"
apply auto
apply (force simp add: bij_is_inj)
--- a/src/HOL/UNITY/Rename.thy Mon Sep 05 23:11:00 2016 +0200
+++ b/src/HOL/UNITY/Rename.thy Mon Sep 05 23:39:15 2016 +0200
@@ -10,7 +10,7 @@
definition rename :: "['a => 'b, 'a program] => 'b program" where
"rename h == extend (%(x,u::unit). h x)"
-declare image_inv_f_f [simp] image_surj_f_inv_f [simp]
+declare image_inv_f_f [simp] image_f_inv_f [simp]
declare Extend.intro [simp,intro]