From d7b9fc814d0fcb296156143a5d9bc3f5d9ad9ad1 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 11 Sep 2018 19:23:21 +0200
Subject: Add the univalence axiom

---
 ProdProps.thy | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'ProdProps.thy')

diff --git a/ProdProps.thy b/ProdProps.thy
index 14556af..47e386b 100644
--- a/ProdProps.thy
+++ b/ProdProps.thy
@@ -49,4 +49,9 @@ proof (subst compose_def, subst Prod_eq)
 qed (derive lems: assms)
 
 
+text "Set up the \<open>compute\<close> method to automatically simplify function compositions."
+
+lemmas compose_comp [comp]
+
+
 end
-- 
cgit v1.2.3