# HG changeset patch
# User wenzelm
# Date 970076086 -7200
# Node ID 44584c2b512b685a6c72bf35bf082d96a859f097
# Parent  4295180d6bab0360acc87105bf5bdd3af254df19
more symbolic syntax (currently "input");

diff -r 4295180d6bab -r 44584c2b512b src/HOL/Record.thy
--- 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 *)