From 64d2a5c60acce40113362c9d7eca8cd633362d23 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 5 Feb 2019 18:32:43 +0100
Subject: Add cong named theorem for congruence rules

---
 HoTT_Base.thy | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'HoTT_Base.thy')

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 88cf986..e74ef31 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -68,16 +68,19 @@ text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type
 
 section \<open>Named theorems\<close>
 
-named_theorems comp
 named_theorems form
+named_theorems comp
+named_theorems cong
 
 text \<open>
 The named theorems above will be used by proof methods defined in @{file HoTT_Methods.thy}.
 
-@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
-
 @{attribute form} declares type formation rules.
 These are mainly used by the \<open>cumulativity\<close> method, which lifts types into higher universes.
+
+@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
+
+@{attribute cong} declares congruence rules, the definitional equality rules of the type theory.
 \<close>
 
 (* Todo: Set up the Simplifier! *)
-- 
cgit v1.2.3