Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added additional parent theory equalities because some proofs in
authorberghofe
Tue, 21 May 1996 13:42:53 +0200
changeset 1755 17001ecd546e
parent 1754 852093aeb0ab
child 1756 978ee7ededdd
Added additional parent theory equalities because some proofs in Prod.ML depend on rules proved in equalities.ML
src/HOL/Prod.thy file | annotate | diff | comparison | revisions 
--- 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 **)
isabelle