src/HOL/Record.thy
changeset 4870 cc36acb5b114
child 5032 0c9939c2ab5c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Record.thy	Wed Apr 29 11:42:04 1998 +0200
     1.3 @@ -0,0 +1,45 @@
     1.4 +(*  Title:      HOL/Record.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Extensible records with structural subtyping in HOL.  See
     1.9 +Tools/record_package.ML for the actual implementation.
    1.10 +*)
    1.11 +
    1.12 +Record = Prod +
    1.13 +
    1.14 +
    1.15 +(* concrete syntax *)
    1.16 +
    1.17 +nonterminals
    1.18 +  ident field fields
    1.19 +
    1.20 +syntax
    1.21 +  ""		    :: "id => ident"			("_")
    1.22 +  ""		    :: "longid => ident"		("_")
    1.23 +  "_field"	    :: "[ident, 'a] => field"		("(2_ =/ _)")
    1.24 +  ""	            :: "field => fields"		("_")
    1.25 +  "_fields"	    :: "[field, fields] => fields"	("_,/ _")
    1.26 +  "_record"	    :: "fields => 'a"			("({: _ :})")
    1.27 +  "_record_scheme"  :: "[fields, 'a] => 'b"		("({: _,/ (2... =/ _) :})")
    1.28 +
    1.29 +
    1.30 +(* type class for record extensions *)
    1.31 +
    1.32 +global		(*compatibility with global_names flag!*)
    1.33 +
    1.34 +axclass more < term
    1.35 +
    1.36 +local
    1.37 +
    1.38 +instance unit :: more
    1.39 +instance "*" :: (term, more) more
    1.40 +
    1.41 +
    1.42 +(* initialize the package *)
    1.43 +
    1.44 +setup
    1.45 +  RecordPackage.setup
    1.46 +
    1.47 +
    1.48 +end