| changeset 80754 | 701912f5645a |
| parent 76381 | 2931d8331cc5 |
| child 80761 | bc936d3d8b45 |
--- a/src/CTT/CTT.thy Fri Aug 23 22:47:51 2024 +0200 +++ b/src/CTT/CTT.thy Fri Aug 23 23:14:39 2024 +0200 @@ -61,6 +61,9 @@ translations "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod(A, \<lambda>x. B)" "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum(A, \<lambda>x. B)" +syntax_consts + "_PROD" \<rightleftharpoons> Prod and + "_SUM" \<rightleftharpoons> Sum abbreviation Arrow :: "[t,t]\<Rightarrow>t" (infixr "\<longrightarrow>" 30) where "A \<longrightarrow> B \<equiv> \<Prod>_:A. B"