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 9729 40cfc3dd27da
parent 7357 d0e16da40ea2
child 10093 44584c2b512b 
--- 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 *)
isabelle