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