src/HOL/Record.thy
changeset 10331 7411e4659d4a
parent 10309 a7f961fb62c6
child 10641 d1533f63c738
     1.1 --- a/src/HOL/Record.thy	Wed Oct 25 18:31:21 2000 +0200
     1.2 +++ b/src/HOL/Record.thy	Wed Oct 25 18:32:02 2000 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4    "_updates"            :: "[update, updates] => updates"               ("_,/ _")
     1.5    "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
     1.6  
     1.7 -syntax (input)   (* FIXME (xsymbols) *)
     1.8 +syntax (xsymbols)
     1.9    "_record_type"        :: "field_types => type"                        ("(3\<lparr>_\<rparr>)")
    1.10    "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
    1.11    "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")