# HG changeset patch
# User huffman
# Date 1272337131 25200
# Node ID d8b26fac82f5281b2f5e537045694c93398e220d
# Parent  e76cb1d4663c5207b981e686c6f45a969274b9d9
remove unused, redundant constant inv_on

diff -r e76cb1d4663c -r d8b26fac82f5 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 19:55:50 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 19:58:51 2010 -0700
@@ -5329,12 +5329,6 @@
 
 text {* Relatively weak hypotheses if a set is compact. *}
 
-definition "inv_on f s = (\<lambda>x. SOME y. y\<in>s \<and> f y = x)"
-
-lemma assumes "inj_on f s" "x\<in>s"
-  shows "inv_on f s (f x) = x"
- using assms unfolding inj_on_def inv_on_def by auto
-
 lemma homeomorphism_compact:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
     (* class constraint due to continuous_on_inverse *)