added type and update syntax;
authorwenzelm
Fri Jul 24 17:54:58 1998 +0200 (1998-07-24)
changeset 5198b1adae4f8b90
parent 5197 69c77ed95ba3
child 5199 be986f7a6def
added type and update syntax;
src/HOL/Record.thy
     1.1 --- a/src/HOL/Record.thy	Fri Jul 24 17:54:44 1998 +0200
     1.2 +++ b/src/HOL/Record.thy	Fri Jul 24 17:54:58 1998 +0200
     1.3 @@ -12,21 +12,37 @@
     1.4  (* concrete syntax *)
     1.5  
     1.6  nonterminals
     1.7 -  ident field fields
     1.8 +  ident field_type field_types field fields update updates
     1.9  
    1.10  syntax
    1.11 -  ""		    :: "id => ident"			("_")
    1.12 -  ""		    :: "longid => ident"		("_")
    1.13 -  "_field"	    :: "[ident, 'a] => field"		("(2_ =/ _)")
    1.14 -  ""	            :: "field => fields"		("_")
    1.15 -  "_fields"	    :: "[field, fields] => fields"	("_,/ _")
    1.16 -  "_record"	    :: "fields => 'a"			("('(| _ |'))")
    1.17 -  "_record_scheme"  :: "[fields, 'a] => 'b"		("('(| _,/ (2... =/ _) |'))")
    1.18 +  (*field names*)
    1.19 +  ""                	:: "id => ident"                    		("_")
    1.20 +  ""                	:: "longid => ident"                		("_")
    1.21 +
    1.22 +  (*record types*)
    1.23 +  "_field_type"         :: "[ident, type] => field_type"           	("(2_ ::/ _)")
    1.24 +  ""               	:: "field_type => field_types"              	("_")
    1.25 +  "_field_types"	:: "[field_type, field_types] => field_types"   ("_,/ _")
    1.26 +  "_record_type"	:: "field_types => type"                   	("('(| _ |'))")
    1.27 +  "_record_type_scheme"	:: "[field_types, type] => type"	("('(| _,/ (2... ::/ _) |'))")
    1.28 +
    1.29 +  (*records*)
    1.30 +  "_field"          	:: "[ident, 'a] => field"           		("(2_ =/ _)")
    1.31 +  ""                	:: "field => fields"                		("_")
    1.32 +  "_fields"         	:: "[field, fields] => fields"      		("_,/ _")
    1.33 +  "_record"         	:: "fields => 'a"                   		("('(| _ |'))")
    1.34 +  "_record_scheme"  	:: "[fields, 'a] => 'a"             	("('(| _,/ (2... =/ _) |'))")
    1.35 +
    1.36 +  (*record updates*)
    1.37 +  "_update"	    	:: "[ident, 'a] => update"           		("(2_ :=/ _)")
    1.38 +  ""                	:: "update => updates"               		("_")
    1.39 +  "_updates"        	:: "[update, updates] => updates"    		("_,/ _")
    1.40 +  "_record_update"  	:: "['a, updates] => 'b"               	("_/('(| _ |'))" [900,0] 900)
    1.41  
    1.42  
    1.43  (* type class for record extensions *)
    1.44  
    1.45 -global		(*compatibility with global_names flag!*)
    1.46 +global          (*compatibility with global_names flag!*)
    1.47  
    1.48  axclass more < term
    1.49