changeset 2278 | d63ffafce255 |
parent 1479 | 21eb5e156d91 |
child 2291 | fbd14a05fb88 |
1.1 --- a/src/HOLCF/Sprod0.thy Fri Nov 29 12:17:30 1996 +0100 1.2 +++ b/src/HOLCF/Sprod0.thy Fri Nov 29 12:22:22 1996 +0100 1.3 @@ -51,6 +51,14 @@ 1.4 &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)" 1.5 1.6 (* start 8bit 1 *) 1.7 +types 1.8 + 1.9 +('a, 'b) "õ" (infixr 20) 1.10 + 1.11 +translations 1.12 + 1.13 +(type) "x õ y" == (type) "x ** y" 1.14 + 1.15 (* end 8bit 1 *) 1.16 1.17 end