diff -r dd877dc7c1f4 -r 6960ec882bca src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Oct 06 14:43:26 1995 +0100
+++ b/src/HOL/Set.thy	Fri Oct 06 16:17:08 1995 +0100
@@ -100,6 +100,9 @@
   inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
   surj_def      "surj(f)        == ! y. ? x. y=f(x)"
 
+(* start 8bit 1 *)
+(* end 8bit 1 *)
+
 end
 
 ML