src/HOL/Nat.thy
changeset 1672 2c109cd2fdd0
parent 1660 8cb42cd97579
child 1674 33aff4d854e4
     1.1 --- a/src/HOL/Nat.thy	Tue Apr 23 16:44:22 1996 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Apr 23 16:58:21 1996 +0200
     1.3 @@ -77,6 +77,11 @@
     1.4    Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
     1.5  
     1.6  (* start 8bit 1 *)
     1.7 +syntax
     1.8 +  "Gmu"	:: (nat => bool) => nat				(binder "" 10)
     1.9 +
    1.10 +translations
    1.11 +  "x.P"	== "LEAST x. P"
    1.12  (* end 8bit 1 *)
    1.13  
    1.14  end