From 41f13f91d023e497d9b35e7a958a961aa0c7a5e5 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 14:34:08 +0200
Subject: Misc formatting

---
 ProdProps.thy | 1 -
 1 file changed, 1 deletion(-)

(limited to 'ProdProps.thy')

diff --git a/ProdProps.thy b/ProdProps.thy
index 7071b39..adadb29 100644
--- a/ProdProps.thy
+++ b/ProdProps.thy
@@ -21,7 +21,6 @@ text "
 lemma compose_assoc:
   assumes "A: U(i)" and "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D(x)"
   shows "(h \<circ> g) \<circ> f \<equiv> h \<circ> (g \<circ> f)"
-
 proof (subst (0 1 2 3) compose_def)
   show "\<^bold>\<lambda>x. (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)"
   proof (subst Prod_eq)
-- 
cgit v1.2.3