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

---
 ex/HoTT book/Ch1.thy | 2 +-
 ex/Synthesis.thy     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'ex')

diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy
index 65de875..cc0adf5 100644
--- a/ex/HoTT book/Ch1.thy	
+++ b/ex/HoTT book/Ch1.thy	
@@ -13,7 +13,7 @@ chapter \<open>HoTT Book, Chapter 1\<close>
 
 section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close>
 
-text "Prove that the only inhabitants of the \<Sigma>-type are those given by the pair constructor."
+text "Propositional uniqueness principle:"
 
 schematic_goal
   assumes "(\<Sum>x:A. B(x)): U(i)" and "p: \<Sum>x:A. B(x)"
diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy
index cd5c4e1..e5a8ecf 100644
--- a/ex/Synthesis.thy
+++ b/ex/Synthesis.thy
@@ -76,4 +76,4 @@ theorem
 by (simple lems: pred_welltyped pred_type pred_props)
 
 
-end
\ No newline at end of file
+end
-- 
cgit v1.2.3