aboutsummaryrefslogtreecommitdiff
path: root/Empty.thy
diff options
context:
space:
mode:
Diffstat (limited to 'Empty.thy')
-rw-r--r--Empty.thy4
1 files changed, 2 insertions, 2 deletions
diff --git a/Empty.thy b/Empty.thy
index a42f7ff..107f2d7 100644
--- a/Empty.thy
+++ b/Empty.thy
@@ -14,8 +14,8 @@ section \<open>Constants and type rules\<close>
section \<open>Empty type\<close>
axiomatization
- Empty :: Term ("\<zero>") and
- indEmpty :: "Term \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)")
+ Empty :: t ("\<zero>") and
+ indEmpty :: "t \<Rightarrow> t" ("(1ind\<^sub>\<zero>)")
where
Empty_form: "\<zero>: U O"
and