src/HOL/Prod.thy

--- a/src/HOL/Prod.thy	Mon Feb 05 14:44:09 1996 +0100
+++ b/src/HOL/Prod.thy	Mon Feb 05 21:27:16 1996 +0100
@@ -19,7 +19,7 @@
 defs
   Pair_Rep_def  "Pair_Rep == (%a b. %x y. x=a & y=b)"
 
-subtype (Prod)
+typedef (Prod)
   ('a, 'b) "*"          (infixr 20)
     = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
 
@@ -61,7 +61,7 @@
 
 (** Unit **)
 
-subtype (Unit)
+typedef (Unit)
   unit = "{p. p = True}"
 
 consts