--- a/src/HOL/Hilbert_Choice.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Hilbert_Choice.thy Mon Mar 01 13:40:23 2010 +0100
@@ -307,8 +307,8 @@
subsection {* Least value operator *}
-constdefs
- LeastM :: "['a => 'b::ord, 'a => bool] => 'a"
+definition
+ LeastM :: "['a => 'b::ord, 'a => bool] => 'a" where
"LeastM m P == SOME x. P x & (\<forall>y. P y --> m x <= m y)"
syntax
@@ -360,11 +360,12 @@
subsection {* Greatest value operator *}
-constdefs
- GreatestM :: "['a => 'b::ord, 'a => bool] => 'a"
+definition
+ GreatestM :: "['a => 'b::ord, 'a => bool] => 'a" where
"GreatestM m P == SOME x. P x & (\<forall>y. P y --> m y <= m x)"
- Greatest :: "('a::ord => bool) => 'a" (binder "GREATEST " 10)
+definition
+ Greatest :: "('a::ord => bool) => 'a" (binder "GREATEST " 10) where
"Greatest == GreatestM (%x. x)"
syntax