src/HOLCF/Holcfb.thy
changeset 1831 fafd8ecbc246
parent 1675 36ba4da350c3
child 1832 79dd1433867c
--- a/src/HOLCF/Holcfb.thy	Wed Jun 26 17:45:32 1996 +0200
+++ b/src/HOLCF/Holcfb.thy	Wed Jun 26 17:50:10 1996 +0200
@@ -17,8 +17,7 @@
 
 theleast_def    "theleast P == (@z.(P z & (!n.P n --> z<=n)))"
 
-(* start 
-   8bit 1 *)
+(* start 8bit 1 *)
 
 syntax
   "Gmu"        :: "[pttrn, bool] => nat"               ("(3´_./ _)" 10)
@@ -26,8 +25,7 @@
 translations
   "´x.P"	== "theleast(%x.P)"
 
-(* end
-   8bit 1 *)
+(* end 8bit 1 *)
 
 end
 *)
\ No newline at end of file