--- a/src/HOL/Nat.thy Wed Apr 17 11:46:10 1996 +0200
+++ b/src/HOL/Nat.thy Wed Apr 17 17:59:58 1996 +0200
@@ -76,4 +76,7 @@
(*least number operator*)
Least_def "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
+(* start 8bit 1 *)
+(* end 8bit 1 *)
+
end