src/HOL/Nat.thy
changeset 1672 2c109cd2fdd0
parent 1660 8cb42cd97579
child 1674 33aff4d854e4
--- 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