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.
\<^bsub>/\<^esub> syntax: unbreakable block;
authorwenzelm
Sat, 29 May 2004 15:11:43 +0200
changeset 14845 345934d5bc1a
parent 14844 a15c65e66ee9
child 14846 b1fcade3880b
\<^bsub>/\<^esub> syntax: unbreakable block;
src/HOL/Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Set.thy	Sat May 29 15:11:06 2004 +0200
+++ b/src/HOL/Set.thy	Sat May 29 15:11:43 2004 +0200
@@ -128,10 +128,10 @@
   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
 
 syntax (xsymbols)
-  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>()\<^bsub>_\<^esub>/ _)" 10)
-  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>()\<^bsub>_\<^esub>/ _)" 10)
-  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
-  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
+  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
+  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
+  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
+  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
 
 
 translations
isabelle