Datatype instead of Prod;
authorwenzelm
Tue Oct 20 16:35:37 1998 +0200 (1998-10-20)
changeset 569439af7b3dd1c4
parent 5693 998af7667fa3
child 5695 898429dbb162
Datatype instead of Prod;
src/HOL/Record.thy
     1.1 --- a/src/HOL/Record.thy	Tue Oct 20 16:33:47 1998 +0200
     1.2 +++ b/src/HOL/Record.thy	Tue Oct 20 16:35:37 1998 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  Tools/record_package.ML for the actual implementation.
     1.5  *)
     1.6  
     1.7 -Record = Prod +
     1.8 +Record = Datatype +
     1.9  
    1.10  
    1.11  (* concrete syntax *)
    1.12 @@ -43,9 +43,7 @@
    1.13  (* type class for record extensions *)
    1.14  
    1.15  axclass more < term
    1.16 -
    1.17  instance unit :: more
    1.18 -instance "*" :: (term, more) more
    1.19  
    1.20  
    1.21  (* initialize the package *)