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