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 +
 1 file changed, 1 insertion(+)

(limited to 'HoTT_Base.thy')

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>
-- 
cgit v1.2.3