diff options
| -rw-r--r-- | Prod.thy | 10 | ||||
| -rw-r--r-- | Sum.thy | 6 |
2 files changed, 8 insertions, 8 deletions
@@ -15,14 +15,14 @@ section \<open>Basic type definitions\<close> axiomatization Prod :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and lam :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and - app :: "[t, t] \<Rightarrow> t" ("(1_ ` _)" [120, 121] 120) + app :: "[t, t] \<Rightarrow> t" ("(2_/ ` _)" [120, 121] 120) \<comment> \<open>Application should bind tighter than abstraction.\<close> syntax - "_Prod" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>'(_: _')./ _)" 30) - "_Prod'" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>_: _./ _)" 30) - "_lam" :: "[idt, t, t] \<Rightarrow> t" ("(3\<lambda>'(_: _')./ _)" 30) - "_lam'" :: "[idt, t, t] \<Rightarrow> t" ("(3\<lambda>_: _./ _)" 30) + "_Prod" :: "[idt, t, t] \<Rightarrow> t" ("(2\<Prod>'(_: _')./ _)" 30) + "_Prod'" :: "[idt, t, t] \<Rightarrow> t" ("(2\<Prod>_: _./ _)" 30) + "_lam" :: "[idt, t, t] \<Rightarrow> t" ("(2\<lambda>'(_: _')./ _)" 30) + "_lam'" :: "[idt, t, t] \<Rightarrow> t" ("(2\<lambda>_: _./ _)" 30) translations "\<Prod>(x: A). B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)" "\<Prod>x: A. B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)" @@ -11,12 +11,12 @@ begin axiomatization Sum :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and - pair :: "[t, t] \<Rightarrow> t" ("(1<_,/ _>)") and + pair :: "[t, t] \<Rightarrow> t" ("(2<_,/ _>)") and indSum :: "[t \<Rightarrow> t, [t, t] \<Rightarrow> t, t] \<Rightarrow> t" syntax - "_Sum" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>'(_: _')./ _)" 20) - "_Sum'" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>_: _./ _)" 20) + "_Sum" :: "[idt, t, t] \<Rightarrow> t" ("(2\<Sum>'(_: _')./ _)" 20) + "_Sum'" :: "[idt, t, t] \<Rightarrow> t" ("(2\<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)" |