Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
\<dots> syntax;
authorwenzelm
Tue, 29 Aug 2000 20:12:54 +0200
changeset 9729 40cfc3dd27da
parent 9728 1546ad1c7839
child 9730 11d137b25555
\<dots> syntax;
src/HOL/Record.thy file | annotate | diff | comparison | revisions 
--- 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