src/Tools/8bit/isa-patches/HOLCF/Ssum0.p
author paulson
Thu, 21 Nov 1996 15:28:25 +0100
changeset 2215 ebf910e7ec87
parent 1826 2a2c0dbeb4ac
permissions -rw-r--r--
Tidied up some proofs, ...
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     1
types
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     2
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     3
('a, 'b) "ó"          (infixr 10)
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     4
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     5
translations
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     6
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     7
(type)  "x ó y"	== (type) "x ++ y" 
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     8