aboutsummaryrefslogtreecommitdiff
path: root/Prod.thy
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Prod.thy1
1 files changed, 1 insertions, 0 deletions
diff --git a/Prod.thy b/Prod.thy
index 5f0d272..162b2e6 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -60,6 +60,7 @@ text "The type rules should be able to be used as introduction and elimination r
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
text "Nondependent functions are a special case."