src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Tue Apr 23 16:44:22 1996 +0200
+++ b/src/HOL/Nat.thy	Tue Apr 23 16:58:21 1996 +0200
@@ -77,6 +77,11 @@
   Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
 
 (* start 8bit 1 *)
+syntax
+  "Gmu"	:: (nat => bool) => nat				(binder "´" 10)
+
+translations
+  "´x.P"	== "LEAST x. P"
 (* end 8bit 1 *)
 
 end