From 7a89ec1e72f61179767c6488177c6d12e69388c5 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 12 Aug 2018 13:04:16 +0200
Subject: Commit before testing polymorphic equality eliminator

---
 Coprod.thy | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'Coprod.thy')

diff --git a/Coprod.thy b/Coprod.thy
index a301e7e..d47c24e 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -44,17 +44,17 @@ and
     \<And>y. y: B \<Longrightarrow> d(y): C(inr(y));
     b: B
     \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(inr(b)) \<equiv> d(b)"
-
+(*
 text "Admissible formation inference rules:"
 
 axiomatization where
   Coprod_form_cond1: "\<And>i A B. A + B: U(i) \<Longrightarrow> A: U(i)"
 and
   Coprod_form_cond2: "\<And>i A B. A + B: U(i) \<Longrightarrow> B: U(i)"
-
-lemmas Coprod_rules [intro] = Coprod_form Coprod_intro1 Coprod_intro2
-                              Coprod_elim Coprod_comp1 Coprod_comp2
-lemmas Coprod_form_conds [intro] = Coprod_form_cond1 Coprod_form_cond2
+*)
+lemmas Coprod_rules [intro] =
+  Coprod_form Coprod_intro1 Coprod_intro2 Coprod_elim Coprod_comp1 Coprod_comp2
+(*lemmas Coprod_form_conds [intro] = Coprod_form_cond1 Coprod_form_cond2 *)
 lemmas Coprod_comps [comp] = Coprod_comp1 Coprod_comp2
 
 
-- 
cgit v1.2.3