Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Record.thy
changeset 61955 e96292f32c3c
parent 61799 4cf66f21b764
child 62117 86a31308a8e1 
--- a/src/HOL/Record.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Record.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -427,26 +427,26 @@
   "_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... ::/ _) |'))")
+  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
+  "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
 
   "_field"              :: "ident => 'a => field"               ("(2_ =/ _)")
   ""                    :: "field => fields"                    ("_")
   "_fields"             :: "field => fields => fields"          ("_,/ _")
-  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
-  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
+  "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
+  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
 
   "_field_update"       :: "ident => 'a => field_update"        ("(2_ :=/ _)")
   ""                    :: "field_update => field_updates"      ("_")
   "_field_updates"      :: "field_update => field_updates => field_updates"  ("_,/ _")
-  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
+  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
 
-syntax (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 => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
+syntax (ASCII)
+  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
+  "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
+  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
+  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
+  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
 
 
 subsection \<open>Record package\<close>
isabelle