# HG changeset patch
# User kleing
# Date 1081944785 -7200
# Node ID c6dc17aab88ace26d0fff1d0455f67b14abe4e95
# Parent  3667b4616e9ab0c76d59e3e370a2d8e1ab00003a
use more symbols in HTML output

diff -r 3667b4616e9a -r c6dc17aab88a src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/CTT/CTT.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -73,6 +73,14 @@
   "@PROD"   :: "[idt,t,t] => t"     ("(3\\<Pi> _\\<in>_./ _)"    10)
   "lam "    :: "[idts, i] => i"     ("(3\\<lambda>\\<lambda>_./ _)" 10)
 
+syntax (HTML output)
+  "@*"      :: "[t,t]=>t"           ("(_ \\<times>/ _)"          [51,50] 50)
+  Elem      :: "[i, t]=>prop"       ("(_ /\\<in> _)" [10,10] 5)
+  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
+  "@SUM"    :: "[idt,t,t] => t"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
+  "@PROD"   :: "[idt,t,t] => t"     ("(3\\<Pi> _\\<in>_./ _)"    10)
+  "lam "    :: "[idts, i] => i"     ("(3\\<lambda>\\<lambda>_./ _)" 10)
+
 rules
 
   (*Reduction: a weaker notion than equality;  a hack for simplification.
diff -r 3667b4616e9a -r c6dc17aab88a src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/FOL/IFOL.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -60,6 +60,12 @@
 
 syntax (HTML output)
   Not           :: "o => o"                     ("\<not> _" [40] 40)
+  "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
+  "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
+  "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
+  "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
+  "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
+  "_not_equal"  :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
 
 
 local
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -746,6 +746,8 @@
   "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_:_. _" [0, 51, 10] 10)
 syntax (xsymbols)
   "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
+syntax (HTML output)
+  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
 translations
   "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
 
@@ -988,6 +990,9 @@
 syntax (xsymbols)
   "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
                 ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
+syntax (HTML output)
+  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
+                ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
 translations
   "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
 
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Fun.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -52,6 +52,8 @@
 
 syntax (xsymbols)
   comp :: "['b => 'c, 'a => 'b, 'a] => 'c"        (infixl "\<circ>" 55)
+syntax (HTML output)
+  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"        (infixl "\<circ>" 55)
 
 
 constdefs
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/HOL.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -102,7 +102,14 @@
   "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
 
 syntax (HTML output)
+  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
   Not           :: "bool => bool"                        ("\<not> _" [40] 40)
+  "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
+  "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
+  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
+  "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
+  "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
+  "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
 
 syntax (HOL)
   "ALL "        :: "[idts, bool] => bool"                ("(3! _./ _)" [0, 10] 10)
@@ -639,6 +646,10 @@
   "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
   "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
 
+syntax (HTML output)
+  "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
+  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
+
 
 lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
 by blast
@@ -1056,6 +1067,12 @@
   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
 
+syntax (HTML output)
+  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
+  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
+  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
+  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
+
 translations
  "ALL x<y. P"   =>  "ALL x. x < y --> P"
  "EX x<y. P"    =>  "EX x. x < y  & P"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -68,6 +68,10 @@
   omega   :: hypreal   ("\<omega>")
   epsilon :: hypreal   ("\<epsilon>")
 
+syntax (HTML output)
+  omega   :: hypreal   ("\<omega>")
+  epsilon :: hypreal   ("\<epsilon>")
+
 
 defs (overloaded)
 
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Hyperreal/IntFloor.thy
--- a/src/HOL/Hyperreal/IntFloor.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Hyperreal/IntFloor.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -20,6 +20,9 @@
   floor :: "real => int"     ("\<lfloor>_\<rfloor>")
   ceiling :: "real => int"   ("\<lceil>_\<rceil>")
 
+syntax (HTML output)
+  floor :: "real => int"     ("\<lfloor>_\<rfloor>")
+  ceiling :: "real => int"   ("\<lceil>_\<rceil>")
 
 
 lemma number_of_less_real_of_int_iff [simp]:
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -43,6 +43,9 @@
 syntax (xsymbols)
     approx :: "[hypreal, hypreal] => bool"    (infixl "\<approx>" 50)
 
+syntax (HTML output)
+    approx :: "[hypreal, hypreal] => bool"    (infixl "\<approx>" 50)
+
 
 
 subsection{*Closure Laws for  Standard Reals*}
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/IMP/Compiler0.thy
--- a/src/HOL/IMP/Compiler0.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/IMP/Compiler0.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -39,6 +39,14 @@
   "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
                ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
 
+syntax (HTML output)
+  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+               ("_ |- (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
+  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
+               ("_ |-/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
+  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
+               ("_ |-/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
+
 translations  
   "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
   "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/IMP/Machines.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -50,6 +50,14 @@
   "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
                ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
 
+syntax (HTML output)
+  "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
+               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
+               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
+               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
+
 translations  
   "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)"
   "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/IMP/Natural.thy
--- a/src/HOL/IMP/Natural.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/IMP/Natural.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -17,6 +17,9 @@
 syntax (xsymbols)
   "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
 
+syntax (HTML output)
+  "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
+
 text {*
   We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started 
   in state @{text s}, terminates in state @{text s'}}. Formally,
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/IMP/Transition.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -35,6 +35,10 @@
   "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
   "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
 
+syntax (HTML output)
+  "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
+  "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
+
 translations
   "\<langle>c,s\<rangle>" == "(Some c, s)"
   "\<langle>s\<rangle>" == "(None, s)"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Induct/QuoDataType.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -26,6 +26,8 @@
   "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "~~" 50)
 syntax (xsymbols)
   "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "\<sim>" 50)
+syntax (HTML output)
+  "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "\<sim>" 50)
 translations
   "X \<sim> Y" == "(X,Y) \<in> msgrel"
 
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)
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Lambda/Type.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -16,6 +16,8 @@
   "e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
 syntax (xsymbols)
   shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+syntax (HTML output)
+  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
 
 lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   by (simp add: shift_def)
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Library/FuncSet.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -30,6 +30,10 @@
   funcset :: "['a set, 'b set] => ('a => 'b) set"  (infixr "\<rightarrow>" 60) 
   "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
 
+syntax (HTML output)
+  "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
+  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
+
 translations
   "PI x:A. B" => "Pi A (%x. B)"
   "A -> B"    => "Pi A (_K B)"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -30,6 +30,9 @@
 syntax (xsymbols)
   Infty :: inat    ("\<infinity>")
 
+syntax (HTML output)
+  Infty :: inat    ("\<infinity>")
+
 defs
   Zero_inat_def: "0 == Fin 0"
   iSuc_def: "iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Library/Word.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -260,6 +260,12 @@
   bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
   bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
 
+syntax (HTML output)
+  bitnot :: "bit => bit"        ("\<not>\<^sub>b _" [40] 40)
+  bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
+  bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
+  bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
+
 primrec
   bitnot_zero: "(bitnot \<zero>) = \<one>"
   bitnot_one : "(bitnot \<one>)  = \<zero>"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/List.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -71,6 +71,8 @@
 
 syntax (xsymbols)
   "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
+syntax (HTML output)
+  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
 
 
 text {*
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -166,6 +166,8 @@
          "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)"
 syntax (xsymbols)
          MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
+syntax (HTML output)
+         MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
 
 lemma MGF_implies_complete:
  "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile>  {P} c {Q} \<Longrightarrow> {} \<turnstile>  {P} c {Q}"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Product_Type.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -159,6 +159,10 @@
   "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
   "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
 
+syntax (HTML output)
+  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
+  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
+
 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
 
 
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Real/HahnBanach/VectorSpace.thy
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -20,6 +20,8 @@
 
 syntax (xsymbols)
   prod  :: "real \<Rightarrow> 'a \<Rightarrow> 'a"                          (infixr "\<cdot>" 70)
+syntax (HTML output)
+  prod  :: "real \<Rightarrow> 'a \<Rightarrow> 'a"                          (infixr "\<cdot>" 70)
 
 
 subsection {* Vector space laws *}
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"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/TLA/Intensional.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -162,7 +162,16 @@
   "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
 
 syntax (HTML output)
+  "_liftNeq"    :: [lift, lift] => lift                (infixl "\\<noteq>" 50)
   "_liftNot"    :: lift => lift                        ("\\<not> _" [40] 40)
+  "_liftAnd"    :: [lift, lift] => lift                (infixr "\\<and>" 35)
+  "_liftOr"     :: [lift, lift] => lift                (infixr "\\<or>" 30)
+  "_RAll"       :: [idts, lift] => lift                ("(3\\<forall>_./ _)" [0, 10] 10)
+  "_REx"        :: [idts, lift] => lift                ("(3\\<exists>_./ _)" [0, 10] 10)
+  "_REx1"       :: [idts, lift] => lift                ("(3\\<exists>!_./ _)" [0, 10] 10)
+  "_liftLeq"    :: [lift, lift] => lift                ("(_/ \\<le> _)" [50, 51] 50)
+  "_liftMem"    :: [lift, lift] => lift                ("(_/ \\<in> _)" [50, 51] 50)
+  "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
 
 rules
   Valid_def   "|- A    ==  ALL w. w |= A"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/TLA/TLA.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -62,6 +62,10 @@
   "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
   "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
 
+syntax (HTML output)
+  "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
+  "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
+
 rules
   (* Definitions of derived operators *)
   dmd_def      "TEMP <>F  ==  TEMP ~[]~F"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Transitive_Closure.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -43,6 +43,11 @@
   trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
   "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
 
+syntax (HTML output)
+  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
+  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
+  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
+
 
 subsection {* Reflexive-transitive closure *}
 
diff -r 3667b4616e9a -r c6dc17aab88a src/HOLCF/IOA/meta_theory/Pred.thy
--- a/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -42,6 +42,8 @@
 
 syntax (HTML output)
   "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
+  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)
+  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)
 
 
 defs
diff -r 3667b4616e9a -r c6dc17aab88a src/HOLCF/Sprod0.thy
--- a/src/HOLCF/Sprod0.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOLCF/Sprod0.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -16,6 +16,8 @@
 
 syntax (xsymbols)
   "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
+syntax (HTML output)
+  "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
 
 consts
   Ispair        :: "['a,'b] => ('a ** 'b)"
diff -r 3667b4616e9a -r c6dc17aab88a src/HOLCF/Ssum0.thy
--- a/src/HOLCF/Ssum0.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOLCF/Ssum0.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -19,6 +19,8 @@
 
 syntax (xsymbols)
   "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
+syntax (HTML output)
+  "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
 
 consts
   Isinl         :: "'a => ('a ++ 'b)"
diff -r 3667b4616e9a -r c6dc17aab88a src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/Pure/Thy/html.ML	Wed Apr 14 14:13:05 2004 +0200
@@ -156,8 +156,8 @@
      | "\\<nabla>" => (1.0, "&nabla;")
      | "\\<in>" => (1.0, "&isin;")
      | "\\<notin>" => (1.0, "&notin;")
-     | "\\<prod>" => (1.0, "&prod;")
-     | "\\<sum>" => (1.0, "&sum;")
+     | "\\<Prod>" => (1.0, "&prod;")
+     | "\\<Sum>" => (1.0, "&sum;")
      | "\\<star>" => (1.0, "&lowast;")
      | "\\<propto>" => (1.0, "&prop;")
      | "\\<infinity>" => (1.0, "&infin;")
diff -r 3667b4616e9a -r c6dc17aab88a src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/Sequents/LK0.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -53,6 +53,12 @@
 
 syntax (HTML output)
   Not           :: o => o               ("\\<not> _" [40] 40)
+  "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
+  "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
+  "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
+  "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
+  "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
+  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
 
 
 local
diff -r 3667b4616e9a -r c6dc17aab88a src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/Cardinal.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -39,6 +39,10 @@
   "lesspoll"    :: "[i,i] => o"       (infixl "\<prec>" 50)
   "LEAST "         :: "[pttrn, o] => i"  ("(3\<mu>_./ _)" [0, 10] 10)
 
+syntax (HTML output)
+  "eqpoll"      :: "[i,i] => o"       (infixl "\<approx>" 50)
+  "LEAST "         :: "[pttrn, o] => i"  ("(3\<mu>_./ _)" [0, 10] 10)
+
 subsection{*The Schroeder-Bernstein Theorem*}
 text{*See Davey and Priestly, page 106*}
 
diff -r 3667b4616e9a -r c6dc17aab88a src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/CardinalArith.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -39,6 +39,9 @@
 syntax (xsymbols)
   "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
   "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
+syntax (HTML output)
+  "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
+  "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
 
 
 lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"
diff -r 3667b4616e9a -r c6dc17aab88a src/ZF/Integ/Int.thy
--- a/src/ZF/Integ/Int.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/Integ/Int.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -82,6 +82,7 @@
 
 syntax (HTML output)
   zmult :: "[i,i]=>i"          (infixl "$\<times>" 70)
+  zle   :: "[i,i]=>o"          (infixl "$\<le>" 50)
 
 
 declare quotientE [elim!]
diff -r 3667b4616e9a -r c6dc17aab88a src/ZF/Main.thy
--- a/src/ZF/Main.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/Main.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -21,6 +21,8 @@
 
 syntax (xsymbols)
   iterates_omega :: "[i=>i,i] => i"   ("(_^\<omega> '(_'))" [60,1000] 60)
+syntax (HTML output)
+  iterates_omega :: "[i=>i,i] => i"   ("(_^\<omega> '(_'))" [60,1000] 60)
 
 lemma iterates_triv:
      "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"  
diff -r 3667b4616e9a -r c6dc17aab88a src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/OrdQuant.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -36,6 +36,10 @@
   "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
   "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
   "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
+syntax (HTML output)
+  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
+  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
+  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
 
 
 subsubsection {*simplification of the new quantifiers*}
@@ -204,6 +208,9 @@
 syntax (xsymbols)
   "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
   "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
+syntax (HTML output)
+  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
+  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
 
 translations
   "ALL x[M]. P"  == "rall(M, %x. P)"
diff -r 3667b4616e9a -r c6dc17aab88a src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/Ordinal.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -34,6 +34,8 @@
 
 syntax (xsymbols)
   "op le"       :: "[i,i] => o"  (infixl "\<le>" 50)  (*less-than or equals*)
+syntax (HTML output)
+  "op le"       :: "[i,i] => o"  (infixl "\<le>" 50)  (*less-than or equals*)
 
 
 subsection{*Rules for Transset*}
diff -r 3667b4616e9a -r c6dc17aab88a src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/ZF/ZF.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -170,6 +170,25 @@
 
 syntax (HTML output)
   "op *"      :: "[i, i] => i"               (infixr "\<times>" 80)
+  "op Int"    :: "[i, i] => i"    	     (infixl "\<inter>" 70)
+  "op Un"     :: "[i, i] => i"    	     (infixl "\<union>" 65)
+  "op <="     :: "[i, i] => o"    	     (infixl "\<subseteq>" 50)
+  "op :"      :: "[i, i] => o"    	     (infixl "\<in>" 50)
+  "op ~:"     :: "[i, i] => o"               (infixl "\<notin>" 50)
+  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
+  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
+  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
+  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
+  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
+  Union       :: "i =>i"                     ("\<Union>_" [90] 90)
+  Inter       :: "i =>i"                     ("\<Inter>_" [90] 90)
+  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
+  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
+  "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
+  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
+  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
+  "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
+  "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
 
 
 finalconsts