src/HOL/Set.thy
changeset 1273 6960ec882bca
parent 1068 e0f2dffab506
child 1370 7361ac9b024d
     1.1 --- a/src/HOL/Set.thy	Fri Oct 06 14:43:26 1995 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri Oct 06 16:17:08 1995 +0100
     1.3 @@ -100,6 +100,9 @@
     1.4    inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     1.5    surj_def      "surj(f)        == ! y. ? x. y=f(x)"
     1.6  
     1.7 +(* start 8bit 1 *)
     1.8 +(* end 8bit 1 *)
     1.9 +
    1.10  end
    1.11  
    1.12  ML