Prod.thy now has the correct definitional equality structure rule. Definition of function composition and properties.

1 files changed, 1 insertions, 1 deletions

diff --git a/Sum.thy b/Sum.thy
index 145c303..8522af1 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -77,4 +77,4 @@ and
 lemmas Empty_rules [intro] = Empty_form Empty_elim
 
 
-end
\ No newline at end of file
+end