From a1afde729f1d9b2f930696b117cfaec827eaa178 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 12 Sep 2018 06:33:55 +0200
Subject: Some final touchups before release 0.1 for the MS thesis

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

(limited to 'ProdProps.thy')

diff --git a/ProdProps.thy b/ProdProps.thy
index 47e386b..a68f79b 100644
--- a/ProdProps.thy
+++ b/ProdProps.thy
@@ -14,7 +14,7 @@ begin
 section \<open>Composition\<close>
 
 text "
-  The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \<Pi>-type definitional equality, and the correct substitutions in the subgoals thereafter.
+  The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \<Prod>-type definitional equality, and the correct substitutions in the subgoals thereafter.
 "
 
 lemma compose_assoc:
-- 
cgit v1.2.3