diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Infinite_Set.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -359,6 +359,10 @@
   "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
   "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
 
+syntax (HTML output)
+  "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
+  "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
+
 lemma INF_EX:
   "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
 proof (unfold INF_def, rule ccontr)