src/HOL/Nat.thy
changeset 1674 33aff4d854e4
parent 1672 2c109cd2fdd0
child 1824 44254696843a
     1.1 --- a/src/HOL/Nat.thy	Tue Apr 23 16:58:57 1996 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Apr 23 17:01:51 1996 +0200
     1.3 @@ -77,11 +77,6 @@
     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