src/HOLCF/Sprod0.thy
changeset 1274 ea0668a1c0ba
parent 1168 74be52691d62
child 1479 21eb5e156d91
--- a/src/HOLCF/Sprod0.thy	Fri Oct 06 16:17:08 1995 +0100
+++ b/src/HOLCF/Sprod0.thy	Fri Oct 06 17:25:24 1995 +0100
@@ -50,5 +50,8 @@
 					(p=Ispair UU UU  --> z=UU)
 		&(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
 
+(* start 8bit 1 *)
+(* end 8bit 1 *)
+
 end