1 files changed, 5 insertions, 5 deletions
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