# HG changeset patch
# User nipkow
# Date 1494758801 -7200
# Node ID 59b945ff568494f46ccbfb98549e1d953498a982
# Parent  3039d4aa71435abec8070b528c65dfb66524aa3a# Parent  416aa3b00cbea0f179bc6ffec03b60f4c5865e75
merged

diff -r 3039d4aa7143 -r 59b945ff5684 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sun May 14 12:06:52 2017 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sun May 14 12:46:41 2017 +0200
@@ -30,11 +30,14 @@
       in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
-definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
-  where "inv_into A f \<equiv> \<lambda>x. SOME y. y \<in> A \<and> f y = x"
+definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
+"inv_into A f = (\<lambda>x. SOME y. y \<in> A \<and> f y = x)"
 
-abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
-  where "inv \<equiv> inv_into UNIV"
+lemma inv_into_def2: "inv_into A f x = (SOME y. y \<in> A \<and> f y = x)"
+by(simp add: inv_into_def)
+
+abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
+"inv \<equiv> inv_into UNIV"
 
 
 subsection \<open>Hilbert's Epsilon-operator\<close>