use more symbols in HTML output
authorkleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565c6dc17aab88a
parent 14564 3667b4616e9a
child 14566 0b60b2edce03
use more symbols in HTML output
src/CTT/CTT.thy
src/FOL/IFOL.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/IntFloor.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/IMP/Compiler0.thy
src/HOL/IMP/Machines.thy
src/HOL/IMP/Natural.thy
src/HOL/IMP/Transition.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Infinite_Set.thy
src/HOL/Lambda/Type.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Word.thy
src/HOL/List.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/Product_Type.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/HOL/Set.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/TLA.thy
src/HOL/Transitive_Closure.thy
src/HOLCF/IOA/meta_theory/Pred.thy
src/HOLCF/Sprod0.thy
src/HOLCF/Ssum0.thy
src/Pure/Thy/html.ML
src/Sequents/LK0.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Integ/Int.thy
src/ZF/Main.thy
src/ZF/OrdQuant.thy
src/ZF/Ordinal.thy
src/ZF/ZF.thy
     1.1 --- a/src/CTT/CTT.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/CTT/CTT.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -73,6 +73,14 @@
     1.4    "@PROD"   :: "[idt,t,t] => t"     ("(3\\<Pi> _\\<in>_./ _)"    10)
     1.5    "lam "    :: "[idts, i] => i"     ("(3\\<lambda>\\<lambda>_./ _)" 10)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  "@*"      :: "[t,t]=>t"           ("(_ \\<times>/ _)"          [51,50] 50)
     1.9 +  Elem      :: "[i, t]=>prop"       ("(_ /\\<in> _)" [10,10] 5)
    1.10 +  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
    1.11 +  "@SUM"    :: "[idt,t,t] => t"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
    1.12 +  "@PROD"   :: "[idt,t,t] => t"     ("(3\\<Pi> _\\<in>_./ _)"    10)
    1.13 +  "lam "    :: "[idts, i] => i"     ("(3\\<lambda>\\<lambda>_./ _)" 10)
    1.14 +
    1.15  rules
    1.16  
    1.17    (*Reduction: a weaker notion than equality;  a hack for simplification.
     2.1 --- a/src/FOL/IFOL.thy	Wed Apr 14 13:28:46 2004 +0200
     2.2 +++ b/src/FOL/IFOL.thy	Wed Apr 14 14:13:05 2004 +0200
     2.3 @@ -60,6 +60,12 @@
     2.4  
     2.5  syntax (HTML output)
     2.6    Not           :: "o => o"                     ("\<not> _" [40] 40)
     2.7 +  "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
     2.8 +  "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
     2.9 +  "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    2.10 +  "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    2.11 +  "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    2.12 +  "_not_equal"  :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    2.13  
    2.14  
    2.15  local
     3.1 --- a/src/HOL/Finite_Set.thy	Wed Apr 14 13:28:46 2004 +0200
     3.2 +++ b/src/HOL/Finite_Set.thy	Wed Apr 14 14:13:05 2004 +0200
     3.3 @@ -746,6 +746,8 @@
     3.4    "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_:_. _" [0, 51, 10] 10)
     3.5  syntax (xsymbols)
     3.6    "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
     3.7 +syntax (HTML output)
     3.8 +  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
     3.9  translations
    3.10    "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
    3.11  
    3.12 @@ -988,6 +990,9 @@
    3.13  syntax (xsymbols)
    3.14    "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
    3.15                  ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
    3.16 +syntax (HTML output)
    3.17 +  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
    3.18 +                ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
    3.19  translations
    3.20    "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
    3.21  
     4.1 --- a/src/HOL/Fun.thy	Wed Apr 14 13:28:46 2004 +0200
     4.2 +++ b/src/HOL/Fun.thy	Wed Apr 14 14:13:05 2004 +0200
     4.3 @@ -52,6 +52,8 @@
     4.4  
     4.5  syntax (xsymbols)
     4.6    comp :: "['b => 'c, 'a => 'b, 'a] => 'c"        (infixl "\<circ>" 55)
     4.7 +syntax (HTML output)
     4.8 +  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"        (infixl "\<circ>" 55)
     4.9  
    4.10  
    4.11  constdefs
     5.1 --- a/src/HOL/HOL.thy	Wed Apr 14 13:28:46 2004 +0200
     5.2 +++ b/src/HOL/HOL.thy	Wed Apr 14 14:13:05 2004 +0200
     5.3 @@ -102,7 +102,14 @@
     5.4    "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
     5.5  
     5.6  syntax (HTML output)
     5.7 +  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
     5.8    Not           :: "bool => bool"                        ("\<not> _" [40] 40)
     5.9 +  "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
    5.10 +  "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
    5.11 +  "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    5.12 +  "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
    5.13 +  "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
    5.14 +  "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
    5.15  
    5.16  syntax (HOL)
    5.17    "ALL "        :: "[idts, bool] => bool"                ("(3! _./ _)" [0, 10] 10)
    5.18 @@ -639,6 +646,10 @@
    5.19    "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    5.20    "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    5.21  
    5.22 +syntax (HTML output)
    5.23 +  "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    5.24 +  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    5.25 +
    5.26  
    5.27  lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
    5.28  by blast
    5.29 @@ -1056,6 +1067,12 @@
    5.30    "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
    5.31    "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
    5.32  
    5.33 +syntax (HTML output)
    5.34 +  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
    5.35 +  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
    5.36 +  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
    5.37 +  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
    5.38 +
    5.39  translations
    5.40   "ALL x<y. P"   =>  "ALL x. x < y --> P"
    5.41   "EX x<y. P"    =>  "EX x. x < y  & P"
     6.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Wed Apr 14 13:28:46 2004 +0200
     6.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Apr 14 14:13:05 2004 +0200
     6.3 @@ -68,6 +68,10 @@
     6.4    omega   :: hypreal   ("\<omega>")
     6.5    epsilon :: hypreal   ("\<epsilon>")
     6.6  
     6.7 +syntax (HTML output)
     6.8 +  omega   :: hypreal   ("\<omega>")
     6.9 +  epsilon :: hypreal   ("\<epsilon>")
    6.10 +
    6.11  
    6.12  defs (overloaded)
    6.13  
     7.1 --- a/src/HOL/Hyperreal/IntFloor.thy	Wed Apr 14 13:28:46 2004 +0200
     7.2 +++ b/src/HOL/Hyperreal/IntFloor.thy	Wed Apr 14 14:13:05 2004 +0200
     7.3 @@ -20,6 +20,9 @@
     7.4    floor :: "real => int"     ("\<lfloor>_\<rfloor>")
     7.5    ceiling :: "real => int"   ("\<lceil>_\<rceil>")
     7.6  
     7.7 +syntax (HTML output)
     7.8 +  floor :: "real => int"     ("\<lfloor>_\<rfloor>")
     7.9 +  ceiling :: "real => int"   ("\<lceil>_\<rceil>")
    7.10  
    7.11  
    7.12  lemma number_of_less_real_of_int_iff [simp]:
     8.1 --- a/src/HOL/Hyperreal/NSA.thy	Wed Apr 14 13:28:46 2004 +0200
     8.2 +++ b/src/HOL/Hyperreal/NSA.thy	Wed Apr 14 14:13:05 2004 +0200
     8.3 @@ -43,6 +43,9 @@
     8.4  syntax (xsymbols)
     8.5      approx :: "[hypreal, hypreal] => bool"    (infixl "\<approx>" 50)
     8.6  
     8.7 +syntax (HTML output)
     8.8 +    approx :: "[hypreal, hypreal] => bool"    (infixl "\<approx>" 50)
     8.9 +
    8.10  
    8.11  
    8.12  subsection{*Closure Laws for  Standard Reals*}
     9.1 --- a/src/HOL/IMP/Compiler0.thy	Wed Apr 14 13:28:46 2004 +0200
     9.2 +++ b/src/HOL/IMP/Compiler0.thy	Wed Apr 14 14:13:05 2004 +0200
     9.3 @@ -39,6 +39,14 @@
     9.4    "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
     9.5                 ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
     9.6  
     9.7 +syntax (HTML output)
     9.8 +  "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
     9.9 +               ("_ |- (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
    9.10 +  "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
    9.11 +               ("_ |-/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
    9.12 +  "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
    9.13 +               ("_ |-/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
    9.14 +
    9.15  translations  
    9.16    "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
    9.17    "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
    10.1 --- a/src/HOL/IMP/Machines.thy	Wed Apr 14 13:28:46 2004 +0200
    10.2 +++ b/src/HOL/IMP/Machines.thy	Wed Apr 14 14:13:05 2004 +0200
    10.3 @@ -50,6 +50,14 @@
    10.4    "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
    10.5                 ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
    10.6  
    10.7 +syntax (HTML output)
    10.8 +  "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
    10.9 +               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
   10.10 +  "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
   10.11 +               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
   10.12 +  "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
   10.13 +               ("(_/ |- (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
   10.14 +
   10.15  translations  
   10.16    "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)"
   10.17    "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*"
    11.1 --- a/src/HOL/IMP/Natural.thy	Wed Apr 14 13:28:46 2004 +0200
    11.2 +++ b/src/HOL/IMP/Natural.thy	Wed Apr 14 14:13:05 2004 +0200
    11.3 @@ -17,6 +17,9 @@
    11.4  syntax (xsymbols)
    11.5    "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
    11.6  
    11.7 +syntax (HTML output)
    11.8 +  "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
    11.9 +
   11.10  text {*
   11.11    We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started 
   11.12    in state @{text s}, terminates in state @{text s'}}. Formally,
    12.1 --- a/src/HOL/IMP/Transition.thy	Wed Apr 14 13:28:46 2004 +0200
    12.2 +++ b/src/HOL/IMP/Transition.thy	Wed Apr 14 14:13:05 2004 +0200
    12.3 @@ -35,6 +35,10 @@
    12.4    "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
    12.5    "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
    12.6  
    12.7 +syntax (HTML output)
    12.8 +  "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
    12.9 +  "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
   12.10 +
   12.11  translations
   12.12    "\<langle>c,s\<rangle>" == "(Some c, s)"
   12.13    "\<langle>s\<rangle>" == "(None, s)"
    13.1 --- a/src/HOL/Induct/QuoDataType.thy	Wed Apr 14 13:28:46 2004 +0200
    13.2 +++ b/src/HOL/Induct/QuoDataType.thy	Wed Apr 14 14:13:05 2004 +0200
    13.3 @@ -26,6 +26,8 @@
    13.4    "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "~~" 50)
    13.5  syntax (xsymbols)
    13.6    "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "\<sim>" 50)
    13.7 +syntax (HTML output)
    13.8 +  "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "\<sim>" 50)
    13.9  translations
   13.10    "X \<sim> Y" == "(X,Y) \<in> msgrel"
   13.11  
    14.1 --- a/src/HOL/Infinite_Set.thy	Wed Apr 14 13:28:46 2004 +0200
    14.2 +++ b/src/HOL/Infinite_Set.thy	Wed Apr 14 14:13:05 2004 +0200
    14.3 @@ -359,6 +359,10 @@
    14.4    "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
    14.5    "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
    14.6  
    14.7 +syntax (HTML output)
    14.8 +  "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
    14.9 +  "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
   14.10 +
   14.11  lemma INF_EX:
   14.12    "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
   14.13  proof (unfold INF_def, rule ccontr)
    15.1 --- a/src/HOL/Lambda/Type.thy	Wed Apr 14 13:28:46 2004 +0200
    15.2 +++ b/src/HOL/Lambda/Type.thy	Wed Apr 14 14:13:05 2004 +0200
    15.3 @@ -16,6 +16,8 @@
    15.4    "e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
    15.5  syntax (xsymbols)
    15.6    shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    15.7 +syntax (HTML output)
    15.8 +  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    15.9  
   15.10  lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   15.11    by (simp add: shift_def)
    16.1 --- a/src/HOL/Library/FuncSet.thy	Wed Apr 14 13:28:46 2004 +0200
    16.2 +++ b/src/HOL/Library/FuncSet.thy	Wed Apr 14 14:13:05 2004 +0200
    16.3 @@ -30,6 +30,10 @@
    16.4    funcset :: "['a set, 'b set] => ('a => 'b) set"  (infixr "\<rightarrow>" 60) 
    16.5    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    16.6  
    16.7 +syntax (HTML output)
    16.8 +  "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    16.9 +  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
   16.10 +
   16.11  translations
   16.12    "PI x:A. B" => "Pi A (%x. B)"
   16.13    "A -> B"    => "Pi A (_K B)"
    17.1 --- a/src/HOL/Library/Nat_Infinity.thy	Wed Apr 14 13:28:46 2004 +0200
    17.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Wed Apr 14 14:13:05 2004 +0200
    17.3 @@ -30,6 +30,9 @@
    17.4  syntax (xsymbols)
    17.5    Infty :: inat    ("\<infinity>")
    17.6  
    17.7 +syntax (HTML output)
    17.8 +  Infty :: inat    ("\<infinity>")
    17.9 +
   17.10  defs
   17.11    Zero_inat_def: "0 == Fin 0"
   17.12    iSuc_def: "iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
    18.1 --- a/src/HOL/Library/Word.thy	Wed Apr 14 13:28:46 2004 +0200
    18.2 +++ b/src/HOL/Library/Word.thy	Wed Apr 14 14:13:05 2004 +0200
    18.3 @@ -260,6 +260,12 @@
    18.4    bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
    18.5    bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
    18.6  
    18.7 +syntax (HTML output)
    18.8 +  bitnot :: "bit => bit"        ("\<not>\<^sub>b _" [40] 40)
    18.9 +  bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
   18.10 +  bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
   18.11 +  bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
   18.12 +
   18.13  primrec
   18.14    bitnot_zero: "(bitnot \<zero>) = \<one>"
   18.15    bitnot_one : "(bitnot \<one>)  = \<zero>"
    19.1 --- a/src/HOL/List.thy	Wed Apr 14 13:28:46 2004 +0200
    19.2 +++ b/src/HOL/List.thy	Wed Apr 14 14:13:05 2004 +0200
    19.3 @@ -71,6 +71,8 @@
    19.4  
    19.5  syntax (xsymbols)
    19.6    "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
    19.7 +syntax (HTML output)
    19.8 +  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])")
    19.9  
   19.10  
   19.11  text {*
    20.1 --- a/src/HOL/NanoJava/Equivalence.thy	Wed Apr 14 13:28:46 2004 +0200
    20.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Wed Apr 14 14:13:05 2004 +0200
    20.3 @@ -166,6 +166,8 @@
    20.4           "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)"
    20.5  syntax (xsymbols)
    20.6           MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
    20.7 +syntax (HTML output)
    20.8 +         MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
    20.9  
   20.10  lemma MGF_implies_complete:
   20.11   "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile>  {P} c {Q} \<Longrightarrow> {} \<turnstile>  {P} c {Q}"
    21.1 --- a/src/HOL/Product_Type.thy	Wed Apr 14 13:28:46 2004 +0200
    21.2 +++ b/src/HOL/Product_Type.thy	Wed Apr 14 14:13:05 2004 +0200
    21.3 @@ -159,6 +159,10 @@
    21.4    "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
    21.5    "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    21.6  
    21.7 +syntax (HTML output)
    21.8 +  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
    21.9 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
   21.10 +
   21.11  print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
   21.12  
   21.13  
    22.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Wed Apr 14 13:28:46 2004 +0200
    22.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Wed Apr 14 14:13:05 2004 +0200
    22.3 @@ -20,6 +20,8 @@
    22.4  
    22.5  syntax (xsymbols)
    22.6    prod  :: "real \<Rightarrow> 'a \<Rightarrow> 'a"                          (infixr "\<cdot>" 70)
    22.7 +syntax (HTML output)
    22.8 +  prod  :: "real \<Rightarrow> 'a \<Rightarrow> 'a"                          (infixr "\<cdot>" 70)
    22.9  
   22.10  
   22.11  subsection {* Vector space laws *}
    23.1 --- a/src/HOL/Set.thy	Wed Apr 14 13:28:46 2004 +0200
    23.2 +++ b/src/HOL/Set.thy	Wed Apr 14 14:13:05 2004 +0200
    23.3 @@ -108,6 +108,20 @@
    23.4    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
    23.5    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
    23.6  
    23.7 +syntax (HTML output)
    23.8 +  "_setle"      :: "'a set => 'a set => bool"             ("op \<subseteq>")
    23.9 +  "_setle"      :: "'a set => 'a set => bool"             ("(_/ \<subseteq> _)" [50, 51] 50)
   23.10 +  "_setless"    :: "'a set => 'a set => bool"             ("op \<subset>")
   23.11 +  "_setless"    :: "'a set => 'a set => bool"             ("(_/ \<subset> _)" [50, 51] 50)
   23.12 +  "op Int"      :: "'a set => 'a set => 'a set"           (infixl "\<inter>" 70)
   23.13 +  "op Un"       :: "'a set => 'a set => 'a set"           (infixl "\<union>" 65)
   23.14 +  "op :"        :: "'a => 'a set => bool"                 ("op \<in>")
   23.15 +  "op :"        :: "'a => 'a set => bool"                 ("(_/ \<in> _)" [50, 51] 50)
   23.16 +  "op ~:"       :: "'a => 'a set => bool"                 ("op \<notin>")
   23.17 +  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ \<notin> _)" [50, 51] 50)
   23.18 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   23.19 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
   23.20 +
   23.21  syntax (input)
   23.22    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" 10)
   23.23    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
   23.24 @@ -120,6 +134,7 @@
   23.25    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>\<^bsub>_\<in>_\<^esub>/ _)" 10)
   23.26    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>\<^bsub>_\<in>_\<^esub>/ _)" 10)
   23.27  
   23.28 +
   23.29  translations
   23.30    "op \<subseteq>" => "op <= :: _ set => _ set => bool"
   23.31    "op \<subset>" => "op <  :: _ set => _ set => bool"
    24.1 --- a/src/HOL/TLA/Intensional.thy	Wed Apr 14 13:28:46 2004 +0200
    24.2 +++ b/src/HOL/TLA/Intensional.thy	Wed Apr 14 14:13:05 2004 +0200
    24.3 @@ -162,7 +162,16 @@
    24.4    "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
    24.5  
    24.6  syntax (HTML output)
    24.7 +  "_liftNeq"    :: [lift, lift] => lift                (infixl "\\<noteq>" 50)
    24.8    "_liftNot"    :: lift => lift                        ("\\<not> _" [40] 40)
    24.9 +  "_liftAnd"    :: [lift, lift] => lift                (infixr "\\<and>" 35)
   24.10 +  "_liftOr"     :: [lift, lift] => lift                (infixr "\\<or>" 30)
   24.11 +  "_RAll"       :: [idts, lift] => lift                ("(3\\<forall>_./ _)" [0, 10] 10)
   24.12 +  "_REx"        :: [idts, lift] => lift                ("(3\\<exists>_./ _)" [0, 10] 10)
   24.13 +  "_REx1"       :: [idts, lift] => lift                ("(3\\<exists>!_./ _)" [0, 10] 10)
   24.14 +  "_liftLeq"    :: [lift, lift] => lift                ("(_/ \\<le> _)" [50, 51] 50)
   24.15 +  "_liftMem"    :: [lift, lift] => lift                ("(_/ \\<in> _)" [50, 51] 50)
   24.16 +  "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
   24.17  
   24.18  rules
   24.19    Valid_def   "|- A    ==  ALL w. w |= A"
    25.1 --- a/src/HOL/TLA/TLA.thy	Wed Apr 14 13:28:46 2004 +0200
    25.2 +++ b/src/HOL/TLA/TLA.thy	Wed Apr 14 14:13:05 2004 +0200
    25.3 @@ -62,6 +62,10 @@
    25.4    "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
    25.5    "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
    25.6  
    25.7 +syntax (HTML output)
    25.8 +  "_EEx"     :: [idts, lift] => lift                ("(3\\<exists>\\<exists> _./ _)" [0,10] 10)
    25.9 +  "_AAll"    :: [idts, lift] => lift                ("(3\\<forall>\\<forall> _./ _)" [0,10] 10)
   25.10 +
   25.11  rules
   25.12    (* Definitions of derived operators *)
   25.13    dmd_def      "TEMP <>F  ==  TEMP ~[]~F"
    26.1 --- a/src/HOL/Transitive_Closure.thy	Wed Apr 14 13:28:46 2004 +0200
    26.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Apr 14 14:13:05 2004 +0200
    26.3 @@ -43,6 +43,11 @@
    26.4    trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
    26.5    "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
    26.6  
    26.7 +syntax (HTML output)
    26.8 +  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
    26.9 +  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
   26.10 +  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
   26.11 +
   26.12  
   26.13  subsection {* Reflexive-transitive closure *}
   26.14  
    27.1 --- a/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Apr 14 13:28:46 2004 +0200
    27.2 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Apr 14 14:13:05 2004 +0200
    27.3 @@ -42,6 +42,8 @@
    27.4  
    27.5  syntax (HTML output)
    27.6    "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
    27.7 +  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)
    27.8 +  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)
    27.9  
   27.10  
   27.11  defs
    28.1 --- a/src/HOLCF/Sprod0.thy	Wed Apr 14 13:28:46 2004 +0200
    28.2 +++ b/src/HOLCF/Sprod0.thy	Wed Apr 14 14:13:05 2004 +0200
    28.3 @@ -16,6 +16,8 @@
    28.4  
    28.5  syntax (xsymbols)
    28.6    "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
    28.7 +syntax (HTML output)
    28.8 +  "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
    28.9  
   28.10  consts
   28.11    Ispair        :: "['a,'b] => ('a ** 'b)"
    29.1 --- a/src/HOLCF/Ssum0.thy	Wed Apr 14 13:28:46 2004 +0200
    29.2 +++ b/src/HOLCF/Ssum0.thy	Wed Apr 14 14:13:05 2004 +0200
    29.3 @@ -19,6 +19,8 @@
    29.4  
    29.5  syntax (xsymbols)
    29.6    "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
    29.7 +syntax (HTML output)
    29.8 +  "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
    29.9  
   29.10  consts
   29.11    Isinl         :: "'a => ('a ++ 'b)"
    30.1 --- a/src/Pure/Thy/html.ML	Wed Apr 14 13:28:46 2004 +0200
    30.2 +++ b/src/Pure/Thy/html.ML	Wed Apr 14 14:13:05 2004 +0200
    30.3 @@ -156,8 +156,8 @@
    30.4       | "\\<nabla>" => (1.0, "&nabla;")
    30.5       | "\\<in>" => (1.0, "&isin;")
    30.6       | "\\<notin>" => (1.0, "&notin;")
    30.7 -     | "\\<prod>" => (1.0, "&prod;")
    30.8 -     | "\\<sum>" => (1.0, "&sum;")
    30.9 +     | "\\<Prod>" => (1.0, "&prod;")
   30.10 +     | "\\<Sum>" => (1.0, "&sum;")
   30.11       | "\\<star>" => (1.0, "&lowast;")
   30.12       | "\\<propto>" => (1.0, "&prop;")
   30.13       | "\\<infinity>" => (1.0, "&infin;")
    31.1 --- a/src/Sequents/LK0.thy	Wed Apr 14 13:28:46 2004 +0200
    31.2 +++ b/src/Sequents/LK0.thy	Wed Apr 14 14:13:05 2004 +0200
    31.3 @@ -53,6 +53,12 @@
    31.4  
    31.5  syntax (HTML output)
    31.6    Not           :: o => o               ("\\<not> _" [40] 40)
    31.7 +  "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
    31.8 +  "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
    31.9 +  "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
   31.10 +  "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
   31.11 +  "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
   31.12 +  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
   31.13  
   31.14  
   31.15  local
    32.1 --- a/src/ZF/Cardinal.thy	Wed Apr 14 13:28:46 2004 +0200
    32.2 +++ b/src/ZF/Cardinal.thy	Wed Apr 14 14:13:05 2004 +0200
    32.3 @@ -39,6 +39,10 @@
    32.4    "lesspoll"    :: "[i,i] => o"       (infixl "\<prec>" 50)
    32.5    "LEAST "         :: "[pttrn, o] => i"  ("(3\<mu>_./ _)" [0, 10] 10)
    32.6  
    32.7 +syntax (HTML output)
    32.8 +  "eqpoll"      :: "[i,i] => o"       (infixl "\<approx>" 50)
    32.9 +  "LEAST "         :: "[pttrn, o] => i"  ("(3\<mu>_./ _)" [0, 10] 10)
   32.10 +
   32.11  subsection{*The Schroeder-Bernstein Theorem*}
   32.12  text{*See Davey and Priestly, page 106*}
   32.13  
    33.1 --- a/src/ZF/CardinalArith.thy	Wed Apr 14 13:28:46 2004 +0200
    33.2 +++ b/src/ZF/CardinalArith.thy	Wed Apr 14 14:13:05 2004 +0200
    33.3 @@ -39,6 +39,9 @@
    33.4  syntax (xsymbols)
    33.5    "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
    33.6    "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
    33.7 +syntax (HTML output)
    33.8 +  "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
    33.9 +  "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
   33.10  
   33.11  
   33.12  lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"
    34.1 --- a/src/ZF/Integ/Int.thy	Wed Apr 14 13:28:46 2004 +0200
    34.2 +++ b/src/ZF/Integ/Int.thy	Wed Apr 14 14:13:05 2004 +0200
    34.3 @@ -82,6 +82,7 @@
    34.4  
    34.5  syntax (HTML output)
    34.6    zmult :: "[i,i]=>i"          (infixl "$\<times>" 70)
    34.7 +  zle   :: "[i,i]=>o"          (infixl "$\<le>" 50)
    34.8  
    34.9  
   34.10  declare quotientE [elim!]
    35.1 --- a/src/ZF/Main.thy	Wed Apr 14 13:28:46 2004 +0200
    35.2 +++ b/src/ZF/Main.thy	Wed Apr 14 14:13:05 2004 +0200
    35.3 @@ -21,6 +21,8 @@
    35.4  
    35.5  syntax (xsymbols)
    35.6    iterates_omega :: "[i=>i,i] => i"   ("(_^\<omega> '(_'))" [60,1000] 60)
    35.7 +syntax (HTML output)
    35.8 +  iterates_omega :: "[i=>i,i] => i"   ("(_^\<omega> '(_'))" [60,1000] 60)
    35.9  
   35.10  lemma iterates_triv:
   35.11       "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"  
    36.1 --- a/src/ZF/OrdQuant.thy	Wed Apr 14 13:28:46 2004 +0200
    36.2 +++ b/src/ZF/OrdQuant.thy	Wed Apr 14 14:13:05 2004 +0200
    36.3 @@ -36,6 +36,10 @@
    36.4    "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    36.5    "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    36.6    "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    36.7 +syntax (HTML output)
    36.8 +  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    36.9 +  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
   36.10 +  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
   36.11  
   36.12  
   36.13  subsubsection {*simplification of the new quantifiers*}
   36.14 @@ -204,6 +208,9 @@
   36.15  syntax (xsymbols)
   36.16    "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
   36.17    "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
   36.18 +syntax (HTML output)
   36.19 +  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
   36.20 +  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
   36.21  
   36.22  translations
   36.23    "ALL x[M]. P"  == "rall(M, %x. P)"
    37.1 --- a/src/ZF/Ordinal.thy	Wed Apr 14 13:28:46 2004 +0200
    37.2 +++ b/src/ZF/Ordinal.thy	Wed Apr 14 14:13:05 2004 +0200
    37.3 @@ -34,6 +34,8 @@
    37.4  
    37.5  syntax (xsymbols)
    37.6    "op le"       :: "[i,i] => o"  (infixl "\<le>" 50)  (*less-than or equals*)
    37.7 +syntax (HTML output)
    37.8 +  "op le"       :: "[i,i] => o"  (infixl "\<le>" 50)  (*less-than or equals*)
    37.9  
   37.10  
   37.11  subsection{*Rules for Transset*}
    38.1 --- a/src/ZF/ZF.thy	Wed Apr 14 13:28:46 2004 +0200
    38.2 +++ b/src/ZF/ZF.thy	Wed Apr 14 14:13:05 2004 +0200
    38.3 @@ -170,6 +170,25 @@
    38.4  
    38.5  syntax (HTML output)
    38.6    "op *"      :: "[i, i] => i"               (infixr "\<times>" 80)
    38.7 +  "op Int"    :: "[i, i] => i"    	     (infixl "\<inter>" 70)
    38.8 +  "op Un"     :: "[i, i] => i"    	     (infixl "\<union>" 65)
    38.9 +  "op <="     :: "[i, i] => o"    	     (infixl "\<subseteq>" 50)
   38.10 +  "op :"      :: "[i, i] => o"    	     (infixl "\<in>" 50)
   38.11 +  "op ~:"     :: "[i, i] => o"               (infixl "\<notin>" 50)
   38.12 +  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
   38.13 +  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
   38.14 +  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
   38.15 +  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
   38.16 +  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
   38.17 +  Union       :: "i =>i"                     ("\<Union>_" [90] 90)
   38.18 +  Inter       :: "i =>i"                     ("\<Inter>_" [90] 90)
   38.19 +  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
   38.20 +  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
   38.21 +  "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
   38.22 +  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
   38.23 +  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
   38.24 +  "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
   38.25 +  "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
   38.26  
   38.27  
   38.28  finalconsts