src/HOL/Prod.thy
changeset 1273 6960ec882bca
parent 1114 c8dfb56a7e95
child 1370 7361ac9b024d
     1.1 --- a/src/HOL/Prod.thy	Fri Oct 06 14:43:26 1995 +0100
     1.2 +++ b/src/HOL/Prod.thy	Fri Oct 06 16:17:08 1995 +0100
     1.3 @@ -74,6 +74,9 @@
     1.4  defs
     1.5    Unity_def     "() == Abs_Unit(True)"
     1.6  
     1.7 +(* start 8bit 1 *)
     1.8 +(* end 8bit 1 *)
     1.9 +
    1.10  end
    1.11  (*
    1.12  ML