src/HOL/Record.thy
author wenzelm
Wed Apr 29 11:42:04 1998 +0200 (1998-04-29)
changeset 4870 cc36acb5b114
child 5032 0c9939c2ab5c
permissions -rw-r--r--
Extensible records with structural subtyping in HOL. See
Tools/record_package.ML for the actual implementation.
     1 (*  Title:      HOL/Record.thy
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     4 
     5 Extensible records with structural subtyping in HOL.  See
     6 Tools/record_package.ML for the actual implementation.
     7 *)
     8 
     9 Record = Prod +
    10 
    11 
    12 (* concrete syntax *)
    13 
    14 nonterminals
    15   ident field fields
    16 
    17 syntax
    18   ""		    :: "id => ident"			("_")
    19   ""		    :: "longid => ident"		("_")
    20   "_field"	    :: "[ident, 'a] => field"		("(2_ =/ _)")
    21   ""	            :: "field => fields"		("_")
    22   "_fields"	    :: "[field, fields] => fields"	("_,/ _")
    23   "_record"	    :: "fields => 'a"			("({: _ :})")
    24   "_record_scheme"  :: "[fields, 'a] => 'b"		("({: _,/ (2... =/ _) :})")
    25 
    26 
    27 (* type class for record extensions *)
    28 
    29 global		(*compatibility with global_names flag!*)
    30 
    31 axclass more < term
    32 
    33 local
    34 
    35 instance unit :: more
    36 instance "*" :: (term, more) more
    37 
    38 
    39 (* initialize the package *)
    40 
    41 setup
    42   RecordPackage.setup
    43 
    44 
    45 end