--- a/src/HOL/Set.thy Wed Feb 11 00:37:18 2004 +0100
+++ b/src/HOL/Set.thy Wed Feb 11 01:26:15 2004 +0100
@@ -103,14 +103,22 @@
"op :" :: "'a => 'a set => bool" ("(_/ \<in> _)" [50, 51] 50)
"op ~:" :: "'a => 'a set => bool" ("op \<notin>")
"op ~:" :: "'a => 'a set => bool" ("(_/ \<notin> _)" [50, 51] 50)
+ Union :: "'a set set => 'a set" ("\<Union>_" [90] 90)
+ Inter :: "'a set set => 'a set" ("\<Inter>_" [90] 90)
+ "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
+ "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
+
+syntax (input)
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" 10)
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" 10)
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" 10)
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" 10)
- Union :: "'a set set => 'a set" ("\<Union>_" [90] 90)
- Inter :: "'a set set => 'a set" ("\<Inter>_" [90] 90)
- "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
- "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 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)
translations
"op \<subseteq>" => "op <= :: _ set => _ set => bool"