# HG changeset patch
# User wenzelm
# Date 967572774 -7200
# Node ID 40cfc3dd27dab017ac66a71b5729d9da0534b81a
# Parent  1546ad1c78396b60fe875a580dd71d810b7abad0
\<dots> syntax;

diff -r 1546ad1c7839 -r 40cfc3dd27da src/HOL/Record.thy
--- a/src/HOL/Record.thy	Tue Aug 29 20:12:35 2000 +0200
+++ b/src/HOL/Record.thy	Tue Aug 29 20:12:54 2000 +0200
@@ -40,6 +40,10 @@
   "_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> =/ _) |'))")
+
 
 (* type class for record extensions *)