diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Set.thy
--- 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"