# HG changeset patch
# User wenzelm
# Date 901295698 -7200
# Node ID b1adae4f8b90285ce7b9497c059b3af56d034f35
# Parent  69c77ed95ba39e30902c91bc1f7b7aa5e4185cd3
added type and update syntax;

diff -r 69c77ed95ba3 -r b1adae4f8b90 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Fri Jul 24 17:54:44 1998 +0200
+++ b/src/HOL/Record.thy	Fri Jul 24 17:54:58 1998 +0200
@@ -12,21 +12,37 @@
 (* concrete syntax *)
 
 nonterminals
-  ident field fields
+  ident field_type field_types field fields update updates
 
 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... =/ _) |'))")
+  (*field names*)
+  ""                	:: "id => ident"                    		("_")
+  ""                	:: "longid => ident"                		("_")
+
+  (*record types*)
+  "_field_type"         :: "[ident, type] => field_type"           	("(2_ ::/ _)")
+  ""               	:: "field_type => field_types"              	("_")
+  "_field_types"	:: "[field_type, field_types] => field_types"   ("_,/ _")
+  "_record_type"	:: "field_types => type"                   	("('(| _ |'))")
+  "_record_type_scheme"	:: "[field_types, type] => type"	("('(| _,/ (2... ::/ _) |'))")
+
+  (*records*)
+  "_field"          	:: "[ident, 'a] => field"           		("(2_ =/ _)")
+  ""                	:: "field => fields"                		("_")
+  "_fields"         	:: "[field, fields] => fields"      		("_,/ _")
+  "_record"         	:: "fields => 'a"                   		("('(| _ |'))")
+  "_record_scheme"  	:: "[fields, 'a] => 'a"             	("('(| _,/ (2... =/ _) |'))")
+
+  (*record updates*)
+  "_update"	    	:: "[ident, 'a] => update"           		("(2_ :=/ _)")
+  ""                	:: "update => updates"               		("_")
+  "_updates"        	:: "[update, updates] => updates"    		("_,/ _")
+  "_record_update"  	:: "['a, updates] => 'b"               	("_/('(| _ |'))" [900,0] 900)
 
 
 (* type class for record extensions *)
 
-global		(*compatibility with global_names flag!*)
+global          (*compatibility with global_names flag!*)
 
 axclass more < term