aboutsummaryrefslogtreecommitdiff
path: root/Unit.thy
diff options
context:
space:
mode:
Diffstat (limited to 'Unit.thy')
-rw-r--r--Unit.thy4
1 files changed, 2 insertions, 2 deletions
diff --git a/Unit.thy b/Unit.thy
index 6adfb02..9b86739 100644
--- a/Unit.thy
+++ b/Unit.thy
@@ -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:"