| changeset 35054 | a5db9779b026 |
| parent 27239 | f2f42f9fa09d |
| child 35762 | af3ff2ba4c54 |
1.1 --- a/src/CTT/CTT.thy Mon Jun 16 22:13:39 2008 +0200 1.2 +++ b/src/CTT/CTT.thy Mon Feb 08 21:28:27 2010 +0100 1.3 @@ -63,8 +63,8 @@ 1.4 "_PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10) 1.5 "_SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10) 1.6 translations 1.7 - "PROD x:A. B" == "Prod(A, %x. B)" 1.8 - "SUM x:A. B" == "Sum(A, %x. B)" 1.9 + "PROD x:A. B" == "CONST Prod(A, %x. B)" 1.10 + "SUM x:A. B" == "CONST Sum(A, %x. B)" 1.11 1.12 abbreviation 1.13 Arrow :: "[t,t]=>t" (infixr "-->" 30) where