Datatype instead of Prod;
authorwenzelm
Tue, 20 Oct 1998 16:35:37 +0200
changeset 5694 39af7b3dd1c4
parent 5693 998af7667fa3
child 5695 898429dbb162
Datatype instead of Prod;
src/HOL/Record.thy
--- a/src/HOL/Record.thy	Tue Oct 20 16:33:47 1998 +0200
+++ b/src/HOL/Record.thy	Tue Oct 20 16:35:37 1998 +0200
@@ -6,7 +6,7 @@
 Tools/record_package.ML for the actual implementation.
 *)
 
-Record = Prod +
+Record = Datatype +
 
 
 (* concrete syntax *)
@@ -43,9 +43,7 @@
 (* type class for record extensions *)
 
 axclass more < term
-
 instance unit :: more
-instance "*" :: (term, more) more
 
 
 (* initialize the package *)