From 8833cdf99d3128466d85eb88aeb8e340e07e937c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 23:27:25 +0200
Subject: Reorganize methods

---
 Prod.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index 323bef4..9dbb01e 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -70,7 +70,7 @@ text "Rule attribute declarations---set up various methods to use the type rules
 
 lemmas Prod_comp [comp] = Prod_appl Prod_uniq
 lemmas Prod_wellform [wellform] = Prod_wellform1 Prod_wellform2
-lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_comp Prod_elim
+lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim
 
 
 section \<open>Function composition\<close>
@@ -97,7 +97,7 @@ and
   Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(\<star>) \<equiv> c"
 
 lemmas Unit_comp [comp]
-lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_comp Unit_elim
+lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
 
 
 end
-- 
cgit v1.2.3