--- a/src/HOL/Hilbert_Choice.thy Sun May 28 11:32:15 2017 +0200
+++ b/src/HOL/Hilbert_Choice.thy Sun May 28 13:57:43 2017 +0200
@@ -522,7 +522,7 @@
lemma tfl_some: "\<forall>P x. P x \<longrightarrow> P (Eps P)"
by (blast intro: someI)
-
+(*
subsection \<open>Greatest value operator\<close>
definition GreatestM :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
@@ -607,7 +607,7 @@
apply (rule GreatestI)
apply assumption+
done
-
+*)
subsection \<open>An aside: bounded accessible part\<close>