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