Rewrote methods: wellformed now two lines, uses named theorems. New, more powerful derive method. Used these to rewrite proofs.

1 files changed, 1 insertions, 2 deletions

diff --git a/Prod.thy b/Prod.thy
index 162b2e6..18582a8 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -59,8 +59,7 @@ This is what the additional formation rules \<open>Prod_form_cond1\<close> and \
 text "The type rules should be able to be used as introduction and elimination rules by the standard reasoner:"
 
 lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
-lemmas Prod_form_conds [elim] = Prod_form_cond1 Prod_form_cond2
-lemmas Prod_simps [simp] = Prod_comp Prod_uniq
+lemmas Prod_form_conds [elim, wellform] = Prod_form_cond1 Prod_form_cond2
 
 text "Nondependent functions are a special case."