aboutsummaryrefslogtreecommitdiff
path: root/Unit.thy
diff options
context:
space:
mode:
authorJosh Chen2018-09-12 06:33:55 +0200
committerJosh Chen2018-09-12 06:33:55 +0200
commita1afde729f1d9b2f930696b117cfaec827eaa178 (patch)
tree651ad0a1413cd911bf81caa862928117015fc6a7 /Unit.thy
parentd7b9fc814d0fcb296156143a5d9bc3f5d9ad9ad1 (diff)
Some final touchups before release 0.1 for the MS thesis
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