aboutsummaryrefslogtreecommitdiff
path: root/ProdProps.thy
diff options
context:
space:
mode:
authorJosh Chen2018-08-18 21:28:21 +0200
committerJosh Chen2018-08-18 21:28:21 +0200
commite1be5f97bb2a42b3179bc24b118d69af137f8e5d (patch)
tree37fa2dacc40261bf37726e23121df0ba5b9af68e /ProdProps.thy
parent03c734ea067bd28210530d862137133e2215ca80 (diff)
Regrouping type rules
Diffstat (limited to 'ProdProps.thy')
-rw-r--r--ProdProps.thy3
1 files changed, 1 insertions, 2 deletions
diff --git a/ProdProps.thy b/ProdProps.thy
index adadb29..3e51102 100644
--- a/ProdProps.thy
+++ b/ProdProps.thy
@@ -1,8 +1,7 @@
(* Title: HoTT/ProdProps.thy
Author: Josh Chen
- Date: Aug 2018
-Properties of the dependent product.
+Properties of the dependent product
*)
theory ProdProps