# HG changeset patch
# User berghofe
# Date 832678973 -7200
# Node ID 17001ecd546ede0ab207ce3ea6447b4bf19b7938
# Parent  852093aeb0abe7c301028f42fc908eb2f7ea21a0
Added additional parent theory equalities because some proofs in
Prod.ML depend on rules proved in equalities.ML

diff -r 852093aeb0ab -r 17001ecd546e src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Tue May 21 13:39:31 1996 +0200
+++ b/src/HOL/Prod.thy	Tue May 21 13:42:53 1996 +0200
@@ -7,7 +7,7 @@
 The unit type.
 *)
 
-Prod = Fun +
+Prod = Fun + equalities +
 
 (** Products **)