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