Prod.thy
changeset 115 0ec63df3ae04
parent 112 3fc2f9c40759
child 185 8325414a370a
--- a/Prod.thy	Thu Aug 18 12:48:03 1994 +0200
+++ b/Prod.thy	Fri Aug 19 11:02:45 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title: 	HOL/prod
+(*  Title: 	HOL/Prod.thy
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
@@ -10,7 +10,7 @@
   Abs_Unit_inverse 	"f: Unit ==> Rep_Unit(Abs_Unit(f)) = f"
 *)
 
-Prod = Set +
+Prod = Fun + 
 
 types   
   ('a,'b) "*"          (infixr 20)