| changeset 11390 | 735bf767833a |
| parent 11389 | 55e2aef8909b |
| child 11391 | e8638d07fdee |
--- a/src/Tools/8bit/isa-patches/HOL/Prod.p Fri Jun 29 18:12:18 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -types - -('a, 'b) "ò" (infixr 20) - -translations - -(type) "x ò y" == (type) "x * y" - - "³(x,y,zs).b" == "split(³x.³(y,zs).b)" - "³(x,y).b" == "split(³x y.b)" -