author | wenzelm |
Tue, 20 Oct 1998 16:35:37 +0200 | |
changeset 5694 | 39af7b3dd1c4 |
parent 5693 | 998af7667fa3 |
child 5695 | 898429dbb162 |
--- 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 *)