diff options
Diffstat (limited to 'Sum.thy')
| -rw-r--r-- | Sum.thy | 12 |
1 files changed, 6 insertions, 6 deletions
@@ -12,13 +12,13 @@ begin section \<open>Constants and syntax\<close> axiomatization - Sum :: "[Term, Typefam] \<Rightarrow> Term" and - pair :: "[Term, Term] \<Rightarrow> Term" ("(1<_,/ _>)") and - indSum :: "[[Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<Sum>)") + Sum :: "[t, Typefam] \<Rightarrow> t" and + pair :: "[t, t] \<Rightarrow> t" ("(1<_,/ _>)") and + indSum :: "[[t, t] \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>\<Sum>)") syntax - "_SUM" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 20) - "_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3SUM _:_./ _)" 20) + "_SUM" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>_:_./ _)" 20) + "_SUM_ASCII" :: "[idt, t, t] \<Rightarrow> t" ("(3SUM _:_./ _)" 20) translations "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" @@ -26,7 +26,7 @@ translations text "Nondependent pair." -abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) +abbreviation Pair :: "[t, t] \<Rightarrow> t" (infixr "\<times>" 50) where "A \<times> B \<equiv> \<Sum>_:A. B" |