Reorganized HoTT_Base, updated theories

1 files changed, 3 insertions, 3 deletions

diff --git a/Unit.thy b/Unit.thy
index 6adfb02..6760f27 100644
--- a/Unit.thy
+++ b/Unit.thy
@@ -16,13 +16,13 @@ axiomatization
   pt :: Term    ("\<star>") and
   indUnit :: "[Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<one>)")
 where
-  Unit_form: "\<one>: U(O)"
+  Unit_form: "\<one>: U O"
 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:"