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