changeset 2291 | fbd14a05fb88 |
parent 2278 | d63ffafce255 |
child 2394 | 91d8abf108be |
1.1 --- a/src/HOLCF/Sprod0.thy Mon Dec 02 12:19:56 1996 +0100 1.2 +++ b/src/HOLCF/Sprod0.thy Mon Dec 02 12:37:15 1996 +0100 1.3 @@ -51,14 +51,6 @@ 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