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 /Empty.thy | |
parent | bed5d559b62cf3f3acb75b28c2e192e274f46cc1 (diff) |
Go back to higher-order application notation
Diffstat (limited to 'Empty.thy')
-rw-r--r-- | Empty.thy | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -17,9 +17,9 @@ axiomatization Empty :: Term ("\<zero>") and indEmpty :: "Term \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)") where - Empty_form: "\<zero>: U(O)" + Empty_form: "\<zero>: U O" and - Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)" + Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U i; z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> z: C z" text "Rule attribute declarations:" |