diff options
| author | Josh Chen | 2019-02-17 18:34:38 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-17 18:34:38 +0100 |
| commit | 68aa069172933b875d70a5ef71e9db0ae685a92d (patch) | |
| tree | bd1da2111e12bab878641661d91f95f66f8132cc /Sum.thy | |
| parent | 76b57317d7568f4dcd673b1b8085601c6c723355 (diff) | |
Method "quantify" converts product inhabitation into Pure universal statements. Also misc. cleanups.
Diffstat (limited to '')
| -rw-r--r-- | Sum.thy | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -18,8 +18,8 @@ syntax "_Sum" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>'(_: _')./ _)" 20) "_Sum'" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>_: _./ _)" 20) translations - "\<Sum>(x: A). B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" - "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" + "\<Sum>(x: A). B" \<rightleftharpoons> "(CONST Sum) A (\<lambda>x. B)" + "\<Sum>x: A. B" \<rightleftharpoons> "(CONST Sum) A (\<lambda>x. B)" abbreviation Pair :: "[t, t] \<Rightarrow> t" (infixr "\<times>" 50) where "A \<times> B \<equiv> \<Sum>_: A. B" |