--- a/src/HOL/Set.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Set.thy Wed Apr 14 14:13:05 2004 +0200
@@ -108,6 +108,20 @@
"_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 (HTML output)
+ "_setle" :: "'a set => 'a set => bool" ("op \<subseteq>")
+ "_setle" :: "'a set => 'a set => bool" ("(_/ \<subseteq> _)" [50, 51] 50)
+ "_setless" :: "'a set => 'a set => bool" ("op \<subset>")
+ "_setless" :: "'a set => 'a set => bool" ("(_/ \<subset> _)" [50, 51] 50)
+ "op Int" :: "'a set => 'a set => 'a set" (infixl "\<inter>" 70)
+ "op Un" :: "'a set => 'a set => 'a set" (infixl "\<union>" 65)
+ "op :" :: "'a => 'a set => bool" ("op \<in>")
+ "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)
+ "_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)
@@ -120,6 +134,7 @@
"@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"
"op \<subset>" => "op < :: _ set => _ set => bool"