From dc2730916482bd230f9bd5244b8b2cc9d005f69a Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 7 Aug 2018 12:30:59 +0200
Subject: Old application syntax incompatible with Eisbach

---
 HoTT_Base.thy | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index c2bb092..614419e 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -9,10 +9,6 @@ theory HoTT_Base
   imports Pure
 begin
 
-text "Use the syntax \<open>f(x)\<close> instead of \<open>f x\<close> for function application."
-
-setup Pure_Thy.old_appl_syntax_setup
-
 
 section \<open>Foundational definitions\<close>
 
-- 
cgit v1.2.3