src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Tue Apr 23 16:58:57 1996 +0200
+++ b/src/HOL/Nat.thy	Tue Apr 23 17:01:51 1996 +0200
@@ -77,11 +77,6 @@
   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