src/HOL/Record.thy
changeset 5732 8712391bbf3d
parent 5694 39af7b3dd1c4
child 7357 d0e16da40ea2
     1.1 --- a/src/HOL/Record.thy	Thu Oct 22 20:13:21 1998 +0200
     1.2 +++ b/src/HOL/Record.thy	Thu Oct 22 20:15:26 1998 +0200
     1.3 @@ -23,21 +23,21 @@
     1.4    "_field_type"         :: "[ident, type] => field_type"           	("(2_ ::/ _)")
     1.5    ""               	:: "field_type => field_types"              	("_")
     1.6    "_field_types"	:: "[field_type, field_types] => field_types"   ("_,/ _")
     1.7 -  "_record_type"	:: "field_types => type"                   	("('(| _ |'))")
     1.8 -  "_record_type_scheme"	:: "[field_types, type] => type"	("('(| _,/ (2... ::/ _) |'))")
     1.9 +  "_record_type"	:: "field_types => type"                   	("(3'(| _ |'))")
    1.10 +  "_record_type_scheme"	:: "[field_types, type] => type"	("(3'(| _,/ (2... ::/ _) |'))")
    1.11  
    1.12    (*records*)
    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] => 'a"             	("('(| _,/ (2... =/ _) |'))")
    1.18 +  "_record"         	:: "fields => 'a"                   		("(3'(| _ |'))")
    1.19 +  "_record_scheme"  	:: "[fields, 'a] => 'a"             	("(3'(| _,/ (2... =/ _) |'))")
    1.20  
    1.21    (*record updates*)
    1.22    "_update"	    	:: "[ident, 'a] => update"           		("(2_ :=/ _)")
    1.23    ""                	:: "update => updates"               		("_")
    1.24    "_updates"        	:: "[update, updates] => updates"    		("_,/ _")
    1.25 -  "_record_update"  	:: "['a, updates] => 'b"               	("_/('(| _ |'))" [900,0] 900)
    1.26 +  "_record_update"  	:: "['a, updates] => 'b"               	("_/(3'(| _ |'))" [900,0] 900)
    1.27  
    1.28  
    1.29  (* type class for record extensions *)