--- 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