src/HOL/Record.thy
changeset 9729 40cfc3dd27da
parent 7357 d0e16da40ea2
child 10093 44584c2b512b
equal deleted inserted replaced
9728:1546ad1c7839 9729:40cfc3dd27da
    38   "_update"	    	:: "[ident, 'a] => update"           		("(2_ :=/ _)")
    38   "_update"	    	:: "[ident, 'a] => update"           		("(2_ :=/ _)")
    39   ""                	:: "update => updates"               		("_")
    39   ""                	:: "update => updates"               		("_")
    40   "_updates"        	:: "[update, updates] => updates"    		("_,/ _")
    40   "_updates"        	:: "[update, updates] => updates"    		("_,/ _")
    41   "_record_update"  	:: "['a, updates] => 'b"               	("_/(3'(| _ |'))" [900,0] 900)
    41   "_record_update"  	:: "['a, updates] => 'b"               	("_/(3'(| _ |'))" [900,0] 900)
    42 
    42 
       
    43 syntax (xsymbols)
       
    44   "_record_type_scheme"	:: "[field_types, type] => type"	("(3'(| _,/ (2\<dots> ::/ _) |'))")
       
    45   "_record_scheme"  	:: "[fields, 'a] => 'a"             	("(3'(| _,/ (2\<dots> =/ _) |'))")
       
    46 
    43 
    47 
    44 (* type class for record extensions *)
    48 (* type class for record extensions *)
    45 
    49 
    46 axclass more < "term"
    50 axclass more < "term"
    47 instance unit :: more
    51 instance unit :: more