author | oheimb |
Wed, 26 Jun 1996 17:50:10 +0200 | |
changeset 1831 | fafd8ecbc246 |
parent 1830 | 861736a24a93 |
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