changeset 35054 | a5db9779b026 |
parent 27239 | f2f42f9fa09d |
child 35762 | af3ff2ba4c54 |
--- a/src/CTT/CTT.thy Mon Feb 08 21:26:52 2010 +0100 +++ b/src/CTT/CTT.thy Mon Feb 08 21:28:27 2010 +0100 @@ -63,8 +63,8 @@ "_PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10) "_SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10) translations - "PROD x:A. B" == "Prod(A, %x. B)" - "SUM x:A. B" == "Sum(A, %x. B)" + "PROD x:A. B" == "CONST Prod(A, %x. B)" + "SUM x:A. B" == "CONST Sum(A, %x. B)" abbreviation Arrow :: "[t,t]=>t" (infixr "-->" 30) where