# HG changeset patch
# User wenzelm
# Date 893842924 -7200
# Node ID cc36acb5b1144e7104fb6ef8277fb646add08c7d
# Parent  f3d30c02c1db0ec0282a7df3be9bb595d50c5be8
Extensible records with structural subtyping in HOL.  See
Tools/record_package.ML for the actual implementation.

diff -r f3d30c02c1db -r cc36acb5b114 src/HOL/Record.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Record.thy	Wed Apr 29 11:42:04 1998 +0200
@@ -0,0 +1,45 @@
+(*  Title:      HOL/Record.thy
+    ID:         $Id$
+    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
+
+Extensible records with structural subtyping in HOL.  See
+Tools/record_package.ML for the actual implementation.
+*)
+
+Record = Prod +
+
+
+(* concrete syntax *)
+
+nonterminals
+  ident field fields
+
+syntax
+  ""		    :: "id => ident"			("_")
+  ""		    :: "longid => ident"		("_")
+  "_field"	    :: "[ident, 'a] => field"		("(2_ =/ _)")
+  ""	            :: "field => fields"		("_")
+  "_fields"	    :: "[field, fields] => fields"	("_,/ _")
+  "_record"	    :: "fields => 'a"			("({: _ :})")
+  "_record_scheme"  :: "[fields, 'a] => 'b"		("({: _,/ (2... =/ _) :})")
+
+
+(* type class for record extensions *)
+
+global		(*compatibility with global_names flag!*)
+
+axclass more < term
+
+local
+
+instance unit :: more
+instance "*" :: (term, more) more
+
+
+(* initialize the package *)
+
+setup
+  RecordPackage.setup
+
+
+end