src/HOL/Record.thy
changeset 7357 d0e16da40ea2
parent 5732 8712391bbf3d
child 9729 40cfc3dd27da
     1.1 --- a/src/HOL/Record.thy	Wed Aug 25 20:46:40 1999 +0200
     1.2 +++ b/src/HOL/Record.thy	Wed Aug 25 20:49:02 1999 +0200
     1.3 @@ -6,7 +6,8 @@
     1.4  Tools/record_package.ML for the actual implementation.
     1.5  *)
     1.6  
     1.7 -Record = Datatype +
     1.8 +theory Record = Datatype
     1.9 +files "Tools/record_package.ML":
    1.10  
    1.11  
    1.12  (* concrete syntax *)
    1.13 @@ -42,8 +43,9 @@
    1.14  
    1.15  (* type class for record extensions *)
    1.16  
    1.17 -axclass more < term
    1.18 +axclass more < "term"
    1.19  instance unit :: more
    1.20 +  by intro_classes
    1.21  
    1.22  
    1.23  (* initialize the package *)