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)