From decb363a30a30c1875bf4b93bc544c28edf3149e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 7 Jul 2018 23:03:33 +0200
Subject: Library snapshot. Methods written, everything nicely organized.

---
 Sum.thy | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Sum.thy')

diff --git a/Sum.thy b/Sum.thy
index fe38960..46bb022 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -9,6 +9,7 @@ theory Sum
   imports HoTT_Base
 begin
 
+
 axiomatization
   Sum :: "[Term, Typefam] \<Rightarrow> Term" and
   pair :: "[Term, Term] \<Rightarrow> Term"  ("(1'(_,/ _'))") and
@@ -54,7 +55,7 @@ lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp
 lemmas Sum_form_conds [elim, wellform] = Sum_form_cond1 Sum_form_cond2
 lemmas Sum_comps [comp] = Sum_comp
 
-\<comment> \<open>Nondependent pair\<close>
+text "Nondependent pair."
 abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
   where "A \<times> B \<equiv> \<Sum>_:A. B"
 
-- 
cgit v1.2.3