--- a/src/HOL/Record.thy Wed Sep 27 11:20:30 2000 +0200
+++ b/src/HOL/Record.thy Wed Sep 27 19:34:46 2000 +0200
@@ -17,32 +17,35 @@
syntax
(*field names*)
- "" :: "id => ident" ("_")
- "" :: "longid => ident" ("_")
+ "" :: "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" ("(3'(| _ |'))")
- "_record_type_scheme" :: "[field_types, type] => type" ("(3'(| _,/ (2... ::/ _) |'))")
+ "_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)")
+ "" :: "field_type => field_types" ("_")
+ "_field_types" :: "[field_type, field_types] => field_types" ("_,/ _")
+ "_record_type" :: "field_types => type" ("(3'(| _ |'))")
+ "_record_type_scheme" :: "[field_types, type] => type" ("(3'(| _,/ (2... ::/ _) |'))")
(*records*)
- "_field" :: "[ident, 'a] => field" ("(2_ =/ _)")
- "" :: "field => fields" ("_")
- "_fields" :: "[field, fields] => fields" ("_,/ _")
- "_record" :: "fields => 'a" ("(3'(| _ |'))")
- "_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2... =/ _) |'))")
+ "_field" :: "[ident, 'a] => field" ("(2_ =/ _)")
+ "" :: "field => fields" ("_")
+ "_fields" :: "[field, fields] => fields" ("_,/ _")
+ "_record" :: "fields => 'a" ("(3'(| _ |'))")
+ "_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2... =/ _) |'))")
(*record updates*)
- "_update" :: "[ident, 'a] => update" ("(2_ :=/ _)")
- "" :: "update => updates" ("_")
- "_updates" :: "[update, updates] => updates" ("_,/ _")
- "_record_update" :: "['a, updates] => 'b" ("_/(3'(| _ |'))" [900,0] 900)
+ "_update" :: "[ident, 'a] => update" ("(2_ :=/ _)")
+ "" :: "update => updates" ("_")
+ "_updates" :: "[update, updates] => updates" ("_,/ _")
+ "_record_update" :: "['a, updates] => 'b" ("_/(3'(| _ |'))" [900,0] 900)
-syntax (xsymbols)
- "_record_type_scheme" :: "[field_types, type] => type" ("(3'(| _,/ (2\<dots> ::/ _) |'))")
- "_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2\<dots> =/ _) |'))")
+syntax (input) (* FIXME (xsymbols) *)
+ "_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)")
+ "_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
+ "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)")
+ "_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
+ "_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
(* type class for record extensions *)