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