diff options
| author | Josh Chen | 2018-09-11 08:59:16 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-09-11 08:59:16 +0200 |
| commit | 9b17aac85aa650a7a9d6463d3d01f1eb228d4572 (patch) | |
| tree | 48fd7cf1d921067e276f2d981ec20f133693baaa /Unit.thy | |
| parent | bed5d559b62cf3f3acb75b28c2e192e274f46cc1 (diff) | |
Go back to higher-order application notation
Diffstat (limited to 'Unit.thy')
| -rw-r--r-- | Unit.thy | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -20,9 +20,9 @@ where and Unit_intro: "\<star>: \<one>" and - Unit_elim: "\<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>); a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(a) : C(a)" + Unit_elim: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>; a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" and - Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(\<star>) \<equiv> c" + Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c" text "Rule attribute declarations:" |