From ad0c2755b011e187792ed90382f72c8808949295 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 8 Mar 2019 17:24:57 +0100
Subject: some options, renaming

---
 HoTT_Base.thy  | 1 +
 More_Types.thy | 2 +-
 Nat.thy        | 2 +-
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index e36b237..9987b78 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -18,6 +18,7 @@ begin
 
 section \<open>Basic setup\<close>
 
+declare[[names_short]]
 declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close>
 
 typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close>
diff --git a/More_Types.thy b/More_Types.thy
index 9125aca..ebbe10b 100644
--- a/More_Types.thy
+++ b/More_Types.thy
@@ -64,7 +64,7 @@ where
 
 lemmas Unit_form [form]
 lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
-lemmas Unit_cmp [comp]
+lemmas Unit_comp [comp] = Unit_cmp
 
 
 section \<open>Empty type\<close>
diff --git a/Nat.thy b/Nat.thy
index 61e03e8..cbfbe2d 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -41,6 +41,6 @@ where
 
 lemmas Nat_form [form]
 lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim
-lemmas Nat_comps [comp] = Nat_cmp_0 Nat_cmp_succ
+lemmas Nat_comp [comp] = Nat_cmp_0 Nat_cmp_succ
 
 end
-- 
cgit v1.2.3