discontinued specific HTML syntax;
authorwenzelm
Fri Oct 09 20:26:03 2015 +0200 (2015-10-09)
changeset 613783e04c9ca001a
parent 61377 517feb558c77
child 61379 c57820ceead3
discontinued specific HTML syntax;
src/CTT/Arith.thy
src/CTT/CTT.thy
src/FOL/IFOL.thy
src/HOL/Archimedean_Field.thy
src/HOL/Filter.thy
src/HOL/Fun.thy
src/HOL/Groups.thy
src/HOL/Groups_Big.thy
src/HOL/Groups_List.thy
src/HOL/HOL.thy
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/IOA/meta_theory/Pred.thy
src/HOL/HOLCF/Sprod.thy
src/HOL/HOLCF/Ssum.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Groups_Big_Fun.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Preorder.thy
src/HOL/List.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/NSA.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Power.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Product_Type.thy
src/HOL/Proofs/Lambda/LambdaType.thy
src/HOL/Set.thy
src/HOL/Set_Interval.thy
src/HOL/Transitive_Closure.thy
src/Sequents/LK0.thy
src/ZF/Arith.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Int_ZF.thy
src/ZF/Main_ZF.thy
src/ZF/OrdQuant.thy
src/ZF/OrderType.thy
src/ZF/Ordinal.thy
src/ZF/ZF.thy
     1.1 --- a/src/CTT/Arith.thy	Fri Oct 09 19:51:20 2015 +0200
     1.2 +++ b/src/CTT/Arith.thy	Fri Oct 09 20:26:03 2015 +0200
     1.3 @@ -39,9 +39,6 @@
     1.4  notation (xsymbols)
     1.5    mult  (infixr "#\<times>" 70)
     1.6  
     1.7 -notation (HTML output)
     1.8 -  mult (infixr "#\<times>" 70)
     1.9 -
    1.10  
    1.11  lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
    1.12  
     2.1 --- a/src/CTT/CTT.thy	Fri Oct 09 19:51:20 2015 +0200
     2.2 +++ b/src/CTT/CTT.thy	Fri Oct 09 20:26:03 2015 +0200
     2.3 @@ -79,20 +79,10 @@
     2.4    Arrow  (infixr "\<longrightarrow>" 30) and
     2.5    Times  (infixr "\<times>" 50)
     2.6  
     2.7 -notation (HTML output)
     2.8 -  lambda  (binder "\<lambda>\<lambda>" 10) and
     2.9 -  Elem  ("(_ /\<in> _)" [10,10] 5) and
    2.10 -  Eqelem  ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
    2.11 -  Times  (infixr "\<times>" 50)
    2.12 -
    2.13  syntax (xsymbols)
    2.14    "_PROD"   :: "[idt,t,t] \<Rightarrow> t"     ("(3\<Pi> _\<in>_./ _)"    10)
    2.15    "_SUM"    :: "[idt,t,t] \<Rightarrow> t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    2.16  
    2.17 -syntax (HTML output)
    2.18 -  "_PROD"   :: "[idt,t,t] \<Rightarrow> t"     ("(3\<Pi> _\<in>_./ _)"    10)
    2.19 -  "_SUM"    :: "[idt,t,t] \<Rightarrow> t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    2.20 -
    2.21    (*Reduction: a weaker notion than equality;  a hack for simplification.
    2.22      Reduce[a,b] means either that  a=b:A  for some A or else that "a" and "b"
    2.23      are textually identical.*)
     3.1 --- a/src/FOL/IFOL.thy	Fri Oct 09 19:51:20 2015 +0200
     3.2 +++ b/src/FOL/IFOL.thy	Fri Oct 09 20:26:03 2015 +0200
     3.3 @@ -96,12 +96,7 @@
     3.4    where "x ~= y == ~ (x = y)"
     3.5  
     3.6  notation (xsymbols)
     3.7 -  not_equal  (infixl "\<noteq>" 50)
     3.8 -
     3.9 -notation (HTML output)
    3.10 -  not_equal  (infixl "\<noteq>" 50)
    3.11 -
    3.12 -notation (xsymbols)
    3.13 +  not_equal  (infixl "\<noteq>" 50) and
    3.14    Not  ("\<not> _" [40] 40) and
    3.15    conj  (infixr "\<and>" 35) and
    3.16    disj  (infixr "\<or>" 30) and
    3.17 @@ -111,14 +106,6 @@
    3.18    imp  (infixr "\<longrightarrow>" 25) and
    3.19    iff  (infixr "\<longleftrightarrow>" 25)
    3.20  
    3.21 -notation (HTML output)
    3.22 -  Not  ("\<not> _" [40] 40) and
    3.23 -  conj  (infixr "\<and>" 35) and
    3.24 -  disj  (infixr "\<or>" 30) and
    3.25 -  All  (binder "\<forall>" 10) and
    3.26 -  Ex  (binder "\<exists>" 10) and
    3.27 -  Ex1  (binder "\<exists>!" 10)
    3.28 -
    3.29  
    3.30  subsection \<open>Lemmas and proof tools\<close>
    3.31  
     4.1 --- a/src/HOL/Archimedean_Field.thy	Fri Oct 09 19:51:20 2015 +0200
     4.2 +++ b/src/HOL/Archimedean_Field.thy	Fri Oct 09 20:26:03 2015 +0200
     4.3 @@ -144,9 +144,6 @@
     4.4  notation (xsymbols)
     4.5    floor  ("\<lfloor>_\<rfloor>")
     4.6  
     4.7 -notation (HTML output)
     4.8 -  floor  ("\<lfloor>_\<rfloor>")
     4.9 -
    4.10  lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
    4.11    using floor_correct [of x] floor_exists1 [of x] by auto
    4.12  
    4.13 @@ -383,9 +380,6 @@
    4.14  notation (xsymbols)
    4.15    ceiling  ("\<lceil>_\<rceil>")
    4.16  
    4.17 -notation (HTML output)
    4.18 -  ceiling  ("\<lceil>_\<rceil>")
    4.19 -
    4.20  lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)"
    4.21    unfolding ceiling_def using floor_correct [of "- x"] by simp
    4.22  
     5.1 --- a/src/HOL/Filter.thy	Fri Oct 09 19:51:20 2015 +0200
     5.2 +++ b/src/HOL/Filter.thy	Fri Oct 09 20:26:03 2015 +0200
     5.3 @@ -698,10 +698,6 @@
     5.4    Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
     5.5    Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
     5.6  
     5.7 -notation (HTML output)
     5.8 -  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
     5.9 -  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
    5.10 -
    5.11  lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
    5.12    unfolding cofinite_def
    5.13  proof (rule eventually_Abs_filter, rule is_filter.intro)
     6.1 --- a/src/HOL/Fun.thy	Fri Oct 09 19:51:20 2015 +0200
     6.2 +++ b/src/HOL/Fun.thy	Fri Oct 09 20:26:03 2015 +0200
     6.3 @@ -48,9 +48,6 @@
     6.4  notation (xsymbols)
     6.5    comp  (infixl "\<circ>" 55)
     6.6  
     6.7 -notation (HTML output)
     6.8 -  comp  (infixl "\<circ>" 55)
     6.9 -
    6.10  lemma comp_apply [simp]: "(f o g) x = f (g x)"
    6.11    by (simp add: comp_def)
    6.12  
     7.1 --- a/src/HOL/Groups.thy	Fri Oct 09 19:51:20 2015 +0200
     7.2 +++ b/src/HOL/Groups.thy	Fri Oct 09 20:26:03 2015 +0200
     7.3 @@ -1206,9 +1206,6 @@
     7.4  notation (xsymbols)
     7.5    abs  ("\<bar>_\<bar>")
     7.6  
     7.7 -notation (HTML output)
     7.8 -  abs  ("\<bar>_\<bar>")
     7.9 -
    7.10  end
    7.11  
    7.12  class sgn =
     8.1 --- a/src/HOL/Groups_Big.thy	Fri Oct 09 19:51:20 2015 +0200
     8.2 +++ b/src/HOL/Groups_Big.thy	Fri Oct 09 20:26:03 2015 +0200
     8.3 @@ -493,8 +493,6 @@
     8.4    "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_./ _)" [0, 51, 10] 10)
     8.5  syntax (xsymbols)
     8.6    "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
     8.7 -syntax (HTML output)
     8.8 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
     8.9  
    8.10  translations -- \<open>Beware of argument permutation!\<close>
    8.11    "SUM i:A. b" == "CONST setsum (%i. b) A"
    8.12 @@ -507,8 +505,6 @@
    8.13    "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
    8.14  syntax (xsymbols)
    8.15    "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
    8.16 -syntax (HTML output)
    8.17 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
    8.18  
    8.19  translations
    8.20    "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
    8.21 @@ -1077,8 +1073,6 @@
    8.22    "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
    8.23  syntax (xsymbols)
    8.24    "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
    8.25 -syntax (HTML output)
    8.26 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
    8.27  
    8.28  translations -- \<open>Beware of argument permutation!\<close>
    8.29    "PROD i:A. b" == "CONST setprod (%i. b) A" 
    8.30 @@ -1091,8 +1085,6 @@
    8.31    "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
    8.32  syntax (xsymbols)
    8.33    "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
    8.34 -syntax (HTML output)
    8.35 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
    8.36  
    8.37  translations
    8.38    "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
     9.1 --- a/src/HOL/Groups_List.thy	Fri Oct 09 19:51:20 2015 +0200
     9.2 +++ b/src/HOL/Groups_List.thy	Fri Oct 09 20:26:03 2015 +0200
     9.3 @@ -107,8 +107,6 @@
     9.4    "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
     9.5  syntax (xsymbols)
     9.6    "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
     9.7 -syntax (HTML output)
     9.8 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
     9.9  
    9.10  translations -- \<open>Beware of argument permutation!\<close>
    9.11    "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
    9.12 @@ -376,8 +374,6 @@
    9.13    "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
    9.14  syntax (xsymbols)
    9.15    "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
    9.16 -syntax (HTML output)
    9.17 -  "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
    9.18  
    9.19  translations -- \<open>Beware of argument permutation!\<close>
    9.20    "PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)"
    10.1 --- a/src/HOL/HOL.thy	Fri Oct 09 19:51:20 2015 +0200
    10.2 +++ b/src/HOL/HOL.thy	Fri Oct 09 20:26:03 2015 +0200
    10.3 @@ -112,12 +112,6 @@
    10.4  notation (xsymbols output)
    10.5    not_equal  (infix "\<noteq>" 50)
    10.6  
    10.7 -notation (HTML output)
    10.8 -  Not  ("\<not> _" [40] 40) and
    10.9 -  conj  (infixr "\<and>" 35) and
   10.10 -  disj  (infixr "\<or>" 30) and
   10.11 -  not_equal  (infix "\<noteq>" 50)
   10.12 -
   10.13  abbreviation (iff)
   10.14    iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "<->" 25) where
   10.15    "A <-> B \<equiv> A = B"
   10.16 @@ -154,11 +148,6 @@
   10.17    Ex  (binder "\<exists>" 10) and
   10.18    Ex1  (binder "\<exists>!" 10)
   10.19  
   10.20 -notation (HTML output)
   10.21 -  All  (binder "\<forall>" 10) and
   10.22 -  Ex  (binder "\<exists>" 10) and
   10.23 -  Ex1  (binder "\<exists>!" 10)
   10.24 -
   10.25  notation (HOL)
   10.26    All  (binder "! " 10) and
   10.27    Ex  (binder "? " 10) and
    11.1 --- a/src/HOL/HOLCF/Cfun.thy	Fri Oct 09 19:51:20 2015 +0200
    11.2 +++ b/src/HOL/HOLCF/Cfun.thy	Fri Oct 09 20:26:03 2015 +0200
    11.3 @@ -27,8 +27,6 @@
    11.4  notation (xsymbols)
    11.5    Rep_cfun  ("(_\<cdot>/_)" [999,1000] 999)
    11.6  
    11.7 -notation (HTML output)
    11.8 -  Rep_cfun  ("(_\<cdot>/_)" [999,1000] 999)
    11.9  
   11.10  subsection {* Syntax for continuous lambda abstraction *}
   11.11  
    12.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Fri Oct 09 19:51:20 2015 +0200
    12.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Fri Oct 09 20:26:03 2015 +0200
    12.3 @@ -39,11 +39,6 @@
    12.4  notation (xsymbols)
    12.5    satisfies  ("_ \<Turnstile> _" [100,9] 8)
    12.6  
    12.7 -notation (HTML output)
    12.8 -  NOT  ("\<not> _" [40] 40) and
    12.9 -  AND  (infixr "\<and>" 35) and
   12.10 -  OR  (infixr "\<or>" 30)
   12.11 -
   12.12  
   12.13  defs
   12.14  
    13.1 --- a/src/HOL/HOLCF/Sprod.thy	Fri Oct 09 19:51:20 2015 +0200
    13.2 +++ b/src/HOL/HOLCF/Sprod.thy	Fri Oct 09 20:26:03 2015 +0200
    13.3 @@ -23,8 +23,7 @@
    13.4  
    13.5  type_notation (xsymbols)
    13.6    sprod  ("(_ \<otimes>/ _)" [21,20] 20)
    13.7 -type_notation (HTML output)
    13.8 -  sprod  ("(_ \<otimes>/ _)" [21,20] 20)
    13.9 +
   13.10  
   13.11  subsection {* Definitions of constants *}
   13.12  
    14.1 --- a/src/HOL/HOLCF/Ssum.thy	Fri Oct 09 19:51:20 2015 +0200
    14.2 +++ b/src/HOL/HOLCF/Ssum.thy	Fri Oct 09 20:26:03 2015 +0200
    14.3 @@ -27,8 +27,6 @@
    14.4  
    14.5  type_notation (xsymbols)
    14.6    ssum  ("(_ \<oplus>/ _)" [21, 20] 20)
    14.7 -type_notation (HTML output)
    14.8 -  ssum  ("(_ \<oplus>/ _)" [21, 20] 20)
    14.9  
   14.10  
   14.11  subsection {* Definitions of constructors *}
    15.1 --- a/src/HOL/Library/Extended_Nat.thy	Fri Oct 09 19:51:20 2015 +0200
    15.2 +++ b/src/HOL/Library/Extended_Nat.thy	Fri Oct 09 20:26:03 2015 +0200
    15.3 @@ -15,8 +15,6 @@
    15.4  notation (xsymbols)
    15.5    infinity  ("\<infinity>")
    15.6  
    15.7 -notation (HTML output)
    15.8 -  infinity  ("\<infinity>")
    15.9  
   15.10  subsection \<open>Type definition\<close>
   15.11  
    16.1 --- a/src/HOL/Library/FuncSet.thy	Fri Oct 09 19:51:20 2015 +0200
    16.2 +++ b/src/HOL/Library/FuncSet.thy	Fri Oct 09 20:26:03 2015 +0200
    16.3 @@ -29,9 +29,6 @@
    16.4  syntax (xsymbols)
    16.5    "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    16.6    "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    16.7 -syntax (HTML output)
    16.8 -  "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    16.9 -  "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
   16.10  translations
   16.11    "\<Pi> x\<in>A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)"
   16.12    "\<lambda>x\<in>A. f" \<rightleftharpoons> "CONST restrict (\<lambda>x. f) A"
   16.13 @@ -357,8 +354,6 @@
   16.14    "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
   16.15  syntax (xsymbols)
   16.16    "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
   16.17 -syntax (HTML output)
   16.18 -  "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
   16.19  translations "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
   16.20  
   16.21  abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^sub>E" 60)
    17.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Fri Oct 09 19:51:20 2015 +0200
    17.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Fri Oct 09 20:26:03 2015 +0200
    17.3 @@ -242,9 +242,6 @@
    17.4    "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3SUM _. _)" [0, 10] 10)
    17.5  syntax (xsymbols)
    17.6    "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
    17.7 -syntax (HTML output)
    17.8 -  "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
    17.9 -
   17.10  translations
   17.11    "\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
   17.12  
   17.13 @@ -318,9 +315,6 @@
   17.14    "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3PROD _. _)" [0, 10] 10)
   17.15  syntax (xsymbols)
   17.16    "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
   17.17 -syntax (HTML output)
   17.18 -  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
   17.19 -
   17.20  translations
   17.21    "\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
   17.22  
    18.1 --- a/src/HOL/Library/Multiset.thy	Fri Oct 09 19:51:20 2015 +0200
    18.2 +++ b/src/HOL/Library/Multiset.thy	Fri Oct 09 20:26:03 2015 +0200
    18.3 @@ -1268,15 +1268,9 @@
    18.4  syntax
    18.5    "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
    18.6        ("(3SUM _:#_. _)" [0, 51, 10] 10)
    18.7 -
    18.8  syntax (xsymbols)
    18.9    "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
   18.10        ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
   18.11 -
   18.12 -syntax (HTML output)
   18.13 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
   18.14 -      ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
   18.15 -
   18.16  translations
   18.17    "SUM i :# A. b" == "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
   18.18  
   18.19 @@ -1322,15 +1316,9 @@
   18.20  syntax
   18.21    "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
   18.22        ("(3PROD _:#_. _)" [0, 51, 10] 10)
   18.23 -
   18.24  syntax (xsymbols)
   18.25    "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
   18.26        ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
   18.27 -
   18.28 -syntax (HTML output)
   18.29 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
   18.30 -      ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
   18.31 -
   18.32  translations
   18.33    "PROD i :# A. b" == "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
   18.34  
    19.1 --- a/src/HOL/Library/Preorder.thy	Fri Oct 09 19:51:20 2015 +0200
    19.2 +++ b/src/HOL/Library/Preorder.thy	Fri Oct 09 20:26:03 2015 +0200
    19.3 @@ -20,10 +20,6 @@
    19.4    equiv ("op \<approx>") and
    19.5    equiv ("(_/ \<approx> _)"  [51, 51] 50)
    19.6  
    19.7 -notation (HTML output)
    19.8 -  equiv ("op \<approx>") and
    19.9 -  equiv ("(_/ \<approx> _)"  [51, 51] 50)
   19.10 -
   19.11  lemma refl [iff]:
   19.12    "x \<approx> x"
   19.13    unfolding equiv_def by simp
    20.1 --- a/src/HOL/List.thy	Fri Oct 09 19:51:20 2015 +0200
    20.2 +++ b/src/HOL/List.thy	Fri Oct 09 20:26:03 2015 +0200
    20.3 @@ -80,15 +80,11 @@
    20.4  syntax
    20.5    -- \<open>Special syntax for filter\<close>
    20.6    "_filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
    20.7 -
    20.8 +syntax (xsymbols)
    20.9 +  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
   20.10  translations
   20.11    "[x<-xs . P]"== "CONST filter (%x. P) xs"
   20.12  
   20.13 -syntax (xsymbols)
   20.14 -  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
   20.15 -syntax (HTML output)
   20.16 -  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
   20.17 -
   20.18  primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   20.19  fold_Nil:  "fold f [] = id" |
   20.20  fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x"
   20.21 @@ -421,8 +417,6 @@
   20.22  
   20.23  syntax (xsymbols)
   20.24    "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
   20.25 -syntax (HTML output)
   20.26 -  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
   20.27  
   20.28  parse_translation \<open>
   20.29    let
    21.1 --- a/src/HOL/NSA/HyperDef.thy	Fri Oct 09 19:51:20 2015 +0200
    21.2 +++ b/src/HOL/NSA/HyperDef.thy	Fri Oct 09 20:26:03 2015 +0200
    21.3 @@ -34,10 +34,6 @@
    21.4    omega  ("\<omega>") and
    21.5    epsilon  ("\<epsilon>")
    21.6  
    21.7 -notation (HTML output)
    21.8 -  omega  ("\<omega>") and
    21.9 -  epsilon  ("\<epsilon>")
   21.10 -
   21.11  
   21.12  subsection {* Real vector class instances *}
   21.13  
    22.1 --- a/src/HOL/NSA/NSA.thy	Fri Oct 09 19:51:20 2015 +0200
    22.2 +++ b/src/HOL/NSA/NSA.thy	Fri Oct 09 20:26:03 2015 +0200
    22.3 @@ -46,9 +46,6 @@
    22.4  notation (xsymbols)
    22.5    approx  (infixl "\<approx>" 50)
    22.6  
    22.7 -notation (HTML output)
    22.8 -  approx  (infixl "\<approx>" 50)
    22.9 -
   22.10  lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}"
   22.11  by (simp add: Reals_def image_def)
   22.12  
    23.1 --- a/src/HOL/NanoJava/Equivalence.thy	Fri Oct 09 19:51:20 2015 +0200
    23.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Fri Oct 09 20:26:03 2015 +0200
    23.3 @@ -165,8 +165,6 @@
    23.4  
    23.5  notation (xsymbols)
    23.6    MGTe  ("MGT\<^sub>e")
    23.7 -notation (HTML output)
    23.8 -  MGTe  ("MGT\<^sub>e")
    23.9  
   23.10  lemma MGF_implies_complete:
   23.11   "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile>  {P} c {Q} \<Longrightarrow> {} \<turnstile>  {P} c {Q}"
    24.1 --- a/src/HOL/Nat.thy	Fri Oct 09 19:51:20 2015 +0200
    24.2 +++ b/src/HOL/Nat.thy	Fri Oct 09 20:26:03 2015 +0200
    24.3 @@ -1317,9 +1317,6 @@
    24.4  notation (latex output)
    24.5    compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    24.6  
    24.7 -notation (HTML output)
    24.8 -  compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    24.9 -
   24.10  text \<open>@{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f}\<close>
   24.11  
   24.12  overloading
    25.1 --- a/src/HOL/Orderings.thy	Fri Oct 09 19:51:20 2015 +0200
    25.2 +++ b/src/HOL/Orderings.thy	Fri Oct 09 20:26:03 2015 +0200
    25.3 @@ -102,10 +102,6 @@
    25.4    less_eq  ("op \<le>") and
    25.5    less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    25.6  
    25.7 -notation (HTML output)
    25.8 -  less_eq  ("op \<le>") and
    25.9 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   25.10 -
   25.11  abbreviation (input)
   25.12    greater_eq  (infix ">=" 50) where
   25.13    "x >= y \<equiv> y <= x"
   25.14 @@ -681,17 +677,6 @@
   25.15    "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3! _<=_./ _)" [0, 0, 10] 10)
   25.16    "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3? _<=_./ _)" [0, 0, 10] 10)
   25.17  
   25.18 -syntax (HTML output)
   25.19 -  "_All_less" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   25.20 -  "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   25.21 -  "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   25.22 -  "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   25.23 -
   25.24 -  "_All_greater" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   25.25 -  "_Ex_greater" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   25.26 -  "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   25.27 -  "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   25.28 -
   25.29  translations
   25.30    "ALL x<y. P"   =>  "ALL x. x < y \<longrightarrow> P"
   25.31    "EX x<y. P"    =>  "EX x. x < y \<and> P"
    26.1 --- a/src/HOL/Power.thy	Fri Oct 09 19:51:20 2015 +0200
    26.2 +++ b/src/HOL/Power.thy	Fri Oct 09 20:26:03 2015 +0200
    26.3 @@ -34,9 +34,6 @@
    26.4  notation (latex output)
    26.5    power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    26.6  
    26.7 -notation (HTML output)
    26.8 -  power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    26.9 -
   26.10  text \<open>Special syntax for squares.\<close>
   26.11  
   26.12  abbreviation (xsymbols)
   26.13 @@ -46,9 +43,6 @@
   26.14  notation (latex output)
   26.15    power2  ("(_\<^sup>2)" [1000] 999)
   26.16  
   26.17 -notation (HTML output)
   26.18 -  power2  ("(_\<^sup>2)" [1000] 999)
   26.19 -
   26.20  end
   26.21  
   26.22  context monoid_mult
    27.1 --- a/src/HOL/Probability/Fin_Map.thy	Fri Oct 09 19:51:20 2015 +0200
    27.2 +++ b/src/HOL/Probability/Fin_Map.thy	Fri Oct 09 20:26:03 2015 +0200
    27.3 @@ -102,13 +102,8 @@
    27.4  
    27.5  syntax
    27.6    "_Pi'"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI' _:_./ _)" 10)
    27.7 -
    27.8  syntax (xsymbols)
    27.9    "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>' _\<in>_./ _)"   10)
   27.10 -
   27.11 -syntax (HTML output)
   27.12 -  "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>' _\<in>_./ _)"   10)
   27.13 -
   27.14  translations
   27.15    "PI' x:A. B" == "CONST Pi' A (%x. B)"
   27.16  
   27.17 @@ -616,13 +611,8 @@
   27.18  
   27.19  syntax
   27.20    "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3PIF _:_./ _)" 10)
   27.21 -
   27.22  syntax (xsymbols)
   27.23    "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^sub>F _\<in>_./ _)"  10)
   27.24 -
   27.25 -syntax (HTML output)
   27.26 -  "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^sub>F _\<in>_./ _)"  10)
   27.27 -
   27.28  translations
   27.29    "PIF x:I. M" == "CONST PiF I (%x. M)"
   27.30  
    28.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Oct 09 19:51:20 2015 +0200
    28.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Oct 09 20:26:03 2015 +0200
    28.3 @@ -170,13 +170,8 @@
    28.4  
    28.5  syntax
    28.6    "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3PIM _:_./ _)" 10)
    28.7 -
    28.8  syntax (xsymbols)
    28.9    "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^sub>M _\<in>_./ _)"  10)
   28.10 -
   28.11 -syntax (HTML output)
   28.12 -  "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^sub>M _\<in>_./ _)"  10)
   28.13 -
   28.14  translations
   28.15    "PIM x:I. M" == "CONST PiM I (%x. M)"
   28.16  
    29.1 --- a/src/HOL/Product_Type.thy	Fri Oct 09 19:51:20 2015 +0200
    29.2 +++ b/src/HOL/Product_Type.thy	Fri Oct 09 20:26:03 2015 +0200
    29.3 @@ -231,8 +231,6 @@
    29.4  
    29.5  type_notation (xsymbols)
    29.6    "prod"  ("(_ \<times>/ _)" [21, 20] 20)
    29.7 -type_notation (HTML output)
    29.8 -  "prod"  ("(_ \<times>/ _)" [21, 20] 20)
    29.9  
   29.10  definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
   29.11    "Pair a b = Abs_prod (Pair_Rep a b)"
   29.12 @@ -1009,9 +1007,6 @@
   29.13  notation (xsymbols)
   29.14    Times  (infixr "\<times>" 80)
   29.15  
   29.16 -notation (HTML output)
   29.17 -  Times  (infixr "\<times>" 80)
   29.18 -
   29.19  hide_const (open) Times
   29.20  
   29.21  syntax
    30.1 --- a/src/HOL/Proofs/Lambda/LambdaType.thy	Fri Oct 09 19:51:20 2015 +0200
    30.2 +++ b/src/HOL/Proofs/Lambda/LambdaType.thy	Fri Oct 09 20:26:03 2015 +0200
    30.3 @@ -17,9 +17,6 @@
    30.4  notation (xsymbols)
    30.5    shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    30.6  
    30.7 -notation (HTML output)
    30.8 -  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    30.9 -
   30.10  lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   30.11    by (simp add: shift_def)
   30.12  
    31.1 --- a/src/HOL/Set.thy	Fri Oct 09 19:51:20 2015 +0200
    31.2 +++ b/src/HOL/Set.thy	Fri Oct 09 20:26:03 2015 +0200
    31.3 @@ -33,12 +33,6 @@
    31.4    not_member  ("op \<notin>") and
    31.5    not_member  ("(_/ \<notin> _)" [51, 51] 50)
    31.6  
    31.7 -notation (HTML output)
    31.8 -  member      ("op \<in>") and
    31.9 -  member      ("(_/ \<in> _)" [51, 51] 50) and
   31.10 -  not_member  ("op \<notin>") and
   31.11 -  not_member  ("(_/ \<notin> _)" [51, 51] 50)
   31.12 -
   31.13  
   31.14  text \<open>Set comprehensions\<close>
   31.15  
   31.16 @@ -167,12 +161,6 @@
   31.17    subset_eq  ("op \<subseteq>") and
   31.18    subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
   31.19  
   31.20 -notation (HTML output)
   31.21 -  subset  ("op \<subset>") and
   31.22 -  subset  ("(_/ \<subset> _)" [51, 51] 50) and
   31.23 -  subset_eq  ("op \<subseteq>") and
   31.24 -  subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
   31.25 -
   31.26  abbreviation (input)
   31.27    supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   31.28    "supset \<equiv> greater"
   31.29 @@ -210,11 +198,6 @@
   31.30    "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
   31.31    "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
   31.32  
   31.33 -syntax (HTML output)
   31.34 -  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   31.35 -  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
   31.36 -  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
   31.37 -
   31.38  translations
   31.39    "ALL x:A. P" == "CONST Ball A (%x. P)"
   31.40    "EX x:A. P" == "CONST Bex A (%x. P)"
   31.41 @@ -242,13 +225,6 @@
   31.42    "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
   31.43    "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3?! _<=_./ _)" [0, 0, 10] 10)
   31.44  
   31.45 -syntax (HTML output)
   31.46 -  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
   31.47 -  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
   31.48 -  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
   31.49 -  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
   31.50 -  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
   31.51 -
   31.52  translations
   31.53   "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"
   31.54   "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"
   31.55 @@ -701,9 +677,6 @@
   31.56  notation (xsymbols)
   31.57    inter  (infixl "\<inter>" 70)
   31.58  
   31.59 -notation (HTML output)
   31.60 -  inter  (infixl "\<inter>" 70)
   31.61 -
   31.62  lemma Int_def:
   31.63    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
   31.64    by (simp add: inf_set_def inf_fun_def)
   31.65 @@ -735,9 +708,6 @@
   31.66  notation (xsymbols)
   31.67    union  (infixl "\<union>" 65)
   31.68  
   31.69 -notation (HTML output)
   31.70 -  union  (infixl "\<union>" 65)
   31.71 -
   31.72  lemma Un_def:
   31.73    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
   31.74    by (simp add: sup_set_def sup_fun_def)
    32.1 --- a/src/HOL/Set_Interval.thy	Fri Oct 09 19:51:20 2015 +0200
    32.2 +++ b/src/HOL/Set_Interval.thy	Fri Oct 09 20:26:03 2015 +0200
    32.3 @@ -1432,11 +1432,6 @@
    32.4    "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
    32.5    "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
    32.6    "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
    32.7 -syntax (HTML output)
    32.8 -  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
    32.9 -  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
   32.10 -  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
   32.11 -  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
   32.12  syntax (latex_sum output)
   32.13    "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
   32.14   ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
   32.15 @@ -1783,11 +1778,6 @@
   32.16    "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
   32.17    "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
   32.18    "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
   32.19 -syntax (HTML output)
   32.20 -  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
   32.21 -  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
   32.22 -  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
   32.23 -  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
   32.24  syntax (latex_prod output)
   32.25    "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
   32.26   ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
    33.1 --- a/src/HOL/Transitive_Closure.thy	Fri Oct 09 19:51:20 2015 +0200
    33.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Oct 09 20:26:03 2015 +0200
    33.3 @@ -59,14 +59,6 @@
    33.4    trancl  ("(_\<^sup>+)" [1000] 999) and
    33.5    reflcl  ("(_\<^sup>=)" [1000] 999)
    33.6  
    33.7 -notation (HTML output)
    33.8 -  rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
    33.9 -  tranclp  ("(_\<^sup>+\<^sup>+)" [1000] 1000) and
   33.10 -  reflclp  ("(_\<^sup>=\<^sup>=)" [1000] 1000) and
   33.11 -  rtrancl  ("(_\<^sup>*)" [1000] 999) and
   33.12 -  trancl  ("(_\<^sup>+)" [1000] 999) and
   33.13 -  reflcl  ("(_\<^sup>=)" [1000] 999)
   33.14 -
   33.15  
   33.16  subsection \<open>Reflexive closure\<close>
   33.17  
    34.1 --- a/src/Sequents/LK0.thy	Fri Oct 09 19:51:20 2015 +0200
    34.2 +++ b/src/Sequents/LK0.thy	Fri Oct 09 20:26:03 2015 +0200
    34.3 @@ -51,14 +51,6 @@
    34.4    Ex  (binder "\<exists>" 10) and
    34.5    not_equal  (infixl "\<noteq>" 50)
    34.6  
    34.7 -notation (HTML output)
    34.8 -  Not  ("\<not> _" [40] 40) and
    34.9 -  conj  (infixr "\<and>" 35) and
   34.10 -  disj  (infixr "\<or>" 30) and
   34.11 -  All  (binder "\<forall>" 10) and
   34.12 -  Ex  (binder "\<exists>" 10) and
   34.13 -  not_equal  (infixl "\<noteq>" 50)
   34.14 -
   34.15  axiomatization where
   34.16  
   34.17    (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
    35.1 --- a/src/ZF/Arith.thy	Fri Oct 09 19:51:20 2015 +0200
    35.2 +++ b/src/ZF/Arith.thy	Fri Oct 09 20:26:03 2015 +0200
    35.3 @@ -75,9 +75,6 @@
    35.4  notation (xsymbols)
    35.5    mult  (infixr "#\<times>" 70)
    35.6  
    35.7 -notation (HTML output)
    35.8 -  mult  (infixr "#\<times>" 70)
    35.9 -
   35.10  declare rec_type [simp]
   35.11          nat_0_le [simp]
   35.12  
    36.1 --- a/src/ZF/Cardinal.thy	Fri Oct 09 19:51:20 2015 +0200
    36.2 +++ b/src/ZF/Cardinal.thy	Fri Oct 09 20:26:03 2015 +0200
    36.3 @@ -42,10 +42,6 @@
    36.4    lesspoll  (infixl "\<prec>" 50) and
    36.5    Least     (binder "\<mu>" 10)
    36.6  
    36.7 -notation (HTML)
    36.8 -  eqpoll    (infixl "\<approx>" 50) and
    36.9 -  Least     (binder "\<mu>" 10)
   36.10 -
   36.11  
   36.12  subsection\<open>The Schroeder-Bernstein Theorem\<close>
   36.13  text\<open>See Davey and Priestly, page 106\<close>
    37.1 --- a/src/ZF/CardinalArith.thy	Fri Oct 09 19:51:20 2015 +0200
    37.2 +++ b/src/ZF/CardinalArith.thy	Fri Oct 09 20:26:03 2015 +0200
    37.3 @@ -43,10 +43,6 @@
    37.4    cadd  (infixl "\<oplus>" 65) and
    37.5    cmult  (infixl "\<otimes>" 70)
    37.6  
    37.7 -notation (HTML)
    37.8 -  cadd  (infixl "\<oplus>" 65) and
    37.9 -  cmult  (infixl "\<otimes>" 70)
   37.10 -
   37.11  
   37.12  lemma Card_Union [simp,intro,TC]:
   37.13    assumes A: "\<And>x. x\<in>A \<Longrightarrow> Card(x)" shows "Card(\<Union>(A))"
    38.1 --- a/src/ZF/Int_ZF.thy	Fri Oct 09 19:51:20 2015 +0200
    38.2 +++ b/src/ZF/Int_ZF.thy	Fri Oct 09 20:26:03 2015 +0200
    38.3 @@ -95,10 +95,6 @@
    38.4    zmult  (infixl "$\<times>" 70) and
    38.5    zle  (infixl "$\<le>" 50)  --\<open>less than or equals\<close>
    38.6  
    38.7 -notation (HTML output)
    38.8 -  zmult  (infixl "$\<times>" 70) and
    38.9 -  zle  (infixl "$\<le>" 50)
   38.10 -
   38.11  
   38.12  declare quotientE [elim!]
   38.13  
    39.1 --- a/src/ZF/Main_ZF.thy	Fri Oct 09 19:51:20 2015 +0200
    39.2 +++ b/src/ZF/Main_ZF.thy	Fri Oct 09 20:26:03 2015 +0200
    39.3 @@ -19,8 +19,6 @@
    39.4  
    39.5  notation (xsymbols)
    39.6    iterates_omega  ("(_^\<omega> '(_'))" [60,1000] 60)
    39.7 -notation (HTML output)
    39.8 -  iterates_omega  ("(_^\<omega> '(_'))" [60,1000] 60)
    39.9  
   39.10  lemma iterates_triv:
   39.11       "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"
    40.1 --- a/src/ZF/OrdQuant.thy	Fri Oct 09 19:51:20 2015 +0200
    40.2 +++ b/src/ZF/OrdQuant.thy	Fri Oct 09 20:26:03 2015 +0200
    40.3 @@ -36,10 +36,6 @@
    40.4    "_oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    40.5    "_oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    40.6    "_OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    40.7 -syntax (HTML output)
    40.8 -  "_oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    40.9 -  "_oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
   40.10 -  "_OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
   40.11  
   40.12  
   40.13  subsubsection \<open>simplification of the new quantifiers\<close>
   40.14 @@ -208,9 +204,6 @@
   40.15  syntax (xsymbols)
   40.16    "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
   40.17    "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
   40.18 -syntax (HTML output)
   40.19 -  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
   40.20 -  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
   40.21  
   40.22  translations
   40.23    "ALL x[M]. P"  == "CONST rall(M, %x. P)"
    41.1 --- a/src/ZF/OrderType.thy	Fri Oct 09 19:51:20 2015 +0200
    41.2 +++ b/src/ZF/OrderType.thy	Fri Oct 09 20:26:03 2015 +0200
    41.3 @@ -52,9 +52,6 @@
    41.4  notation (xsymbols)
    41.5    omult  (infixl "\<times>\<times>" 70)
    41.6  
    41.7 -notation (HTML output)
    41.8 -  omult  (infixl "\<times>\<times>" 70)
    41.9 -
   41.10  
   41.11  subsection\<open>Proofs needing the combination of Ordinal.thy and Order.thy\<close>
   41.12  
    42.1 --- a/src/ZF/Ordinal.thy	Fri Oct 09 19:51:20 2015 +0200
    42.2 +++ b/src/ZF/Ordinal.thy	Fri Oct 09 20:26:03 2015 +0200
    42.3 @@ -34,9 +34,6 @@
    42.4  notation (xsymbols)
    42.5    le  (infixl "\<le>" 50)
    42.6  
    42.7 -notation (HTML output)
    42.8 -  le  (infixl "\<le>" 50)
    42.9 -
   42.10  
   42.11  subsection\<open>Rules for Transset\<close>
   42.12  
    43.1 --- a/src/ZF/ZF.thy	Fri Oct 09 19:51:20 2015 +0200
    43.2 +++ b/src/ZF/ZF.thy	Fri Oct 09 20:26:03 2015 +0200
    43.3 @@ -171,31 +171,6 @@
    43.4    "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
    43.5    "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
    43.6  
    43.7 -notation (HTML output)
    43.8 -  cart_prod       (infixr "\<times>" 80) and
    43.9 -  Int             (infixl "\<inter>" 70) and
   43.10 -  Un              (infixl "\<union>" 65) and
   43.11 -  Subset          (infixl "\<subseteq>" 50) and
   43.12 -  mem             (infixl "\<in>" 50) and
   43.13 -  not_mem         (infixl "\<notin>" 50) and
   43.14 -  Union           ("\<Union>_" [90] 90) and
   43.15 -  Inter           ("\<Inter>_" [90] 90)
   43.16 -
   43.17 -syntax (HTML output)
   43.18 -  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
   43.19 -  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
   43.20 -  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
   43.21 -  "_UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
   43.22 -  "_INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
   43.23 -  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
   43.24 -  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
   43.25 -  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
   43.26 -  "_Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
   43.27 -  "_Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
   43.28 -  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
   43.29 -  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
   43.30 -
   43.31 -
   43.32  defs  (* Bounded Quantifiers *)
   43.33    Ball_def:      "Ball(A, P) == \<forall>x. x\<in>A \<longrightarrow> P(x)"
   43.34    Bex_def:       "Bex(A, P) == \<exists>x. x\<in>A & P(x)"