# HG changeset patch
# User wenzelm
# Date 1473111555 -7200
# Node ID 5f77017055a385e05b01e202b7a76d98b12b5b19
# Parent  c54a53ef18730d183600fa786eae8153e48e93ad
clarified obscure facts;

diff -r c54a53ef1873 -r 5f77017055a3 NEWS
--- 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:
diff -r c54a53ef1873 -r 5f77017055a3 src/HOL/Analysis/Polytope.thy
--- 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
diff -r c54a53ef1873 -r 5f77017055a3 src/HOL/Hilbert_Choice.thy
--- 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)
diff -r c54a53ef1873 -r 5f77017055a3 src/HOL/UNITY/Rename.thy
--- 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]