src/HOL/Nat.thy
changeset 1660 8cb42cd97579
parent 1625 40501958d0f6
child 1672 2c109cd2fdd0
     1.1 --- a/src/HOL/Nat.thy	Wed Apr 17 11:46:10 1996 +0200
     1.2 +++ b/src/HOL/Nat.thy	Wed Apr 17 17:59:58 1996 +0200
     1.3 @@ -76,4 +76,7 @@
     1.4    (*least number operator*)
     1.5    Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
     1.6  
     1.7 +(* start 8bit 1 *)
     1.8 +(* end 8bit 1 *)
     1.9 +
    1.10  end