--- a/src/CTT/Arith.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/CTT/Arith.thy Fri Oct 09 20:26:03 2015 +0200
@@ -39,9 +39,6 @@
notation (xsymbols)
mult (infixr "#\<times>" 70)
-notation (HTML output)
- mult (infixr "#\<times>" 70)
-
lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
--- a/src/CTT/CTT.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/CTT/CTT.thy Fri Oct 09 20:26:03 2015 +0200
@@ -79,20 +79,10 @@
Arrow (infixr "\<longrightarrow>" 30) and
Times (infixr "\<times>" 50)
-notation (HTML output)
- lambda (binder "\<lambda>\<lambda>" 10) and
- Elem ("(_ /\<in> _)" [10,10] 5) and
- Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
- Times (infixr "\<times>" 50)
-
syntax (xsymbols)
"_PROD" :: "[idt,t,t] \<Rightarrow> t" ("(3\<Pi> _\<in>_./ _)" 10)
"_SUM" :: "[idt,t,t] \<Rightarrow> t" ("(3\<Sigma> _\<in>_./ _)" 10)
-syntax (HTML output)
- "_PROD" :: "[idt,t,t] \<Rightarrow> t" ("(3\<Pi> _\<in>_./ _)" 10)
- "_SUM" :: "[idt,t,t] \<Rightarrow> t" ("(3\<Sigma> _\<in>_./ _)" 10)
-
(*Reduction: a weaker notion than equality; a hack for simplification.
Reduce[a,b] means either that a=b:A for some A or else that "a" and "b"
are textually identical.*)
--- a/src/FOL/IFOL.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/FOL/IFOL.thy Fri Oct 09 20:26:03 2015 +0200
@@ -96,12 +96,7 @@
where "x ~= y == ~ (x = y)"
notation (xsymbols)
- not_equal (infixl "\<noteq>" 50)
-
-notation (HTML output)
- not_equal (infixl "\<noteq>" 50)
-
-notation (xsymbols)
+ not_equal (infixl "\<noteq>" 50) and
Not ("\<not> _" [40] 40) and
conj (infixr "\<and>" 35) and
disj (infixr "\<or>" 30) and
@@ -111,14 +106,6 @@
imp (infixr "\<longrightarrow>" 25) and
iff (infixr "\<longleftrightarrow>" 25)
-notation (HTML output)
- Not ("\<not> _" [40] 40) and
- conj (infixr "\<and>" 35) and
- disj (infixr "\<or>" 30) and
- All (binder "\<forall>" 10) and
- Ex (binder "\<exists>" 10) and
- Ex1 (binder "\<exists>!" 10)
-
subsection \<open>Lemmas and proof tools\<close>
--- a/src/HOL/Archimedean_Field.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Archimedean_Field.thy Fri Oct 09 20:26:03 2015 +0200
@@ -144,9 +144,6 @@
notation (xsymbols)
floor ("\<lfloor>_\<rfloor>")
-notation (HTML output)
- floor ("\<lfloor>_\<rfloor>")
-
lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
using floor_correct [of x] floor_exists1 [of x] by auto
@@ -383,9 +380,6 @@
notation (xsymbols)
ceiling ("\<lceil>_\<rceil>")
-notation (HTML output)
- ceiling ("\<lceil>_\<rceil>")
-
lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)"
unfolding ceiling_def using floor_correct [of "- x"] by simp
--- a/src/HOL/Filter.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Filter.thy Fri Oct 09 20:26:03 2015 +0200
@@ -698,10 +698,6 @@
Inf_many (binder "\<exists>\<^sub>\<infinity>" 10) and
Alm_all (binder "\<forall>\<^sub>\<infinity>" 10)
-notation (HTML output)
- Inf_many (binder "\<exists>\<^sub>\<infinity>" 10) and
- Alm_all (binder "\<forall>\<^sub>\<infinity>" 10)
-
lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
unfolding cofinite_def
proof (rule eventually_Abs_filter, rule is_filter.intro)
--- a/src/HOL/Fun.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Fun.thy Fri Oct 09 20:26:03 2015 +0200
@@ -48,9 +48,6 @@
notation (xsymbols)
comp (infixl "\<circ>" 55)
-notation (HTML output)
- comp (infixl "\<circ>" 55)
-
lemma comp_apply [simp]: "(f o g) x = f (g x)"
by (simp add: comp_def)
--- a/src/HOL/Groups.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Groups.thy Fri Oct 09 20:26:03 2015 +0200
@@ -1206,9 +1206,6 @@
notation (xsymbols)
abs ("\<bar>_\<bar>")
-notation (HTML output)
- abs ("\<bar>_\<bar>")
-
end
class sgn =
--- a/src/HOL/Groups_Big.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Groups_Big.thy Fri Oct 09 20:26:03 2015 +0200
@@ -493,8 +493,6 @@
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_./ _)" [0, 51, 10] 10)
syntax (xsymbols)
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
-syntax (HTML output)
- "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
translations -- \<open>Beware of argument permutation!\<close>
"SUM i:A. b" == "CONST setsum (%i. b) A"
@@ -507,8 +505,6 @@
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
syntax (xsymbols)
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
-syntax (HTML output)
- "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
translations
"SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
@@ -1077,8 +1073,6 @@
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD _:_./ _)" [0, 51, 10] 10)
syntax (xsymbols)
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
-syntax (HTML output)
- "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
translations -- \<open>Beware of argument permutation!\<close>
"PROD i:A. b" == "CONST setprod (%i. b) A"
@@ -1091,8 +1085,6 @@
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
syntax (xsymbols)
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
-syntax (HTML output)
- "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
translations
"PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
--- a/src/HOL/Groups_List.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Groups_List.thy Fri Oct 09 20:26:03 2015 +0200
@@ -107,8 +107,6 @@
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
syntax (xsymbols)
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
-syntax (HTML output)
- "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
translations -- \<open>Beware of argument permutation!\<close>
"SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
@@ -376,8 +374,6 @@
"_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10)
syntax (xsymbols)
"_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
-syntax (HTML output)
- "_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
translations -- \<open>Beware of argument permutation!\<close>
"PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)"
--- a/src/HOL/HOL.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/HOL.thy Fri Oct 09 20:26:03 2015 +0200
@@ -112,12 +112,6 @@
notation (xsymbols output)
not_equal (infix "\<noteq>" 50)
-notation (HTML output)
- Not ("\<not> _" [40] 40) and
- conj (infixr "\<and>" 35) and
- disj (infixr "\<or>" 30) and
- not_equal (infix "\<noteq>" 50)
-
abbreviation (iff)
iff :: "[bool, bool] \<Rightarrow> bool" (infixr "<->" 25) where
"A <-> B \<equiv> A = B"
@@ -154,11 +148,6 @@
Ex (binder "\<exists>" 10) and
Ex1 (binder "\<exists>!" 10)
-notation (HTML output)
- All (binder "\<forall>" 10) and
- Ex (binder "\<exists>" 10) and
- Ex1 (binder "\<exists>!" 10)
-
notation (HOL)
All (binder "! " 10) and
Ex (binder "? " 10) and
--- a/src/HOL/HOLCF/Cfun.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Fri Oct 09 20:26:03 2015 +0200
@@ -27,8 +27,6 @@
notation (xsymbols)
Rep_cfun ("(_\<cdot>/_)" [999,1000] 999)
-notation (HTML output)
- Rep_cfun ("(_\<cdot>/_)" [999,1000] 999)
subsection {* Syntax for continuous lambda abstraction *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Fri Oct 09 20:26:03 2015 +0200
@@ -39,11 +39,6 @@
notation (xsymbols)
satisfies ("_ \<Turnstile> _" [100,9] 8)
-notation (HTML output)
- NOT ("\<not> _" [40] 40) and
- AND (infixr "\<and>" 35) and
- OR (infixr "\<or>" 30)
-
defs
--- a/src/HOL/HOLCF/Sprod.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/HOLCF/Sprod.thy Fri Oct 09 20:26:03 2015 +0200
@@ -23,8 +23,7 @@
type_notation (xsymbols)
sprod ("(_ \<otimes>/ _)" [21,20] 20)
-type_notation (HTML output)
- sprod ("(_ \<otimes>/ _)" [21,20] 20)
+
subsection {* Definitions of constants *}
--- a/src/HOL/HOLCF/Ssum.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/HOLCF/Ssum.thy Fri Oct 09 20:26:03 2015 +0200
@@ -27,8 +27,6 @@
type_notation (xsymbols)
ssum ("(_ \<oplus>/ _)" [21, 20] 20)
-type_notation (HTML output)
- ssum ("(_ \<oplus>/ _)" [21, 20] 20)
subsection {* Definitions of constructors *}
--- a/src/HOL/Library/Extended_Nat.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Fri Oct 09 20:26:03 2015 +0200
@@ -15,8 +15,6 @@
notation (xsymbols)
infinity ("\<infinity>")
-notation (HTML output)
- infinity ("\<infinity>")
subsection \<open>Type definition\<close>
--- a/src/HOL/Library/FuncSet.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Library/FuncSet.thy Fri Oct 09 20:26:03 2015 +0200
@@ -29,9 +29,6 @@
syntax (xsymbols)
"_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
"_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
-syntax (HTML output)
- "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
- "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
translations
"\<Pi> x\<in>A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)"
"\<lambda>x\<in>A. f" \<rightleftharpoons> "CONST restrict (\<lambda>x. f) A"
@@ -357,8 +354,6 @@
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PIE _:_./ _)" 10)
syntax (xsymbols)
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
-syntax (HTML output)
- "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
translations "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^sub>E" 60)
--- a/src/HOL/Library/Groups_Big_Fun.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Fri Oct 09 20:26:03 2015 +0200
@@ -242,9 +242,6 @@
"_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _. _)" [0, 10] 10)
syntax (xsymbols)
"_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_. _)" [0, 10] 10)
-syntax (HTML output)
- "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_. _)" [0, 10] 10)
-
translations
"\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
@@ -318,9 +315,6 @@
"_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3PROD _. _)" [0, 10] 10)
syntax (xsymbols)
"_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3\<Prod>_. _)" [0, 10] 10)
-syntax (HTML output)
- "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3\<Prod>_. _)" [0, 10] 10)
-
translations
"\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
--- a/src/HOL/Library/Multiset.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Oct 09 20:26:03 2015 +0200
@@ -1268,15 +1268,9 @@
syntax
"_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
("(3SUM _:#_. _)" [0, 51, 10] 10)
-
syntax (xsymbols)
"_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
-
-syntax (HTML output)
- "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
- ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
-
translations
"SUM i :# A. b" == "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
@@ -1322,15 +1316,9 @@
syntax
"_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
("(3PROD _:#_. _)" [0, 51, 10] 10)
-
syntax (xsymbols)
"_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
-
-syntax (HTML output)
- "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
- ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
-
translations
"PROD i :# A. b" == "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
--- a/src/HOL/Library/Preorder.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Library/Preorder.thy Fri Oct 09 20:26:03 2015 +0200
@@ -20,10 +20,6 @@
equiv ("op \<approx>") and
equiv ("(_/ \<approx> _)" [51, 51] 50)
-notation (HTML output)
- equiv ("op \<approx>") and
- equiv ("(_/ \<approx> _)" [51, 51] 50)
-
lemma refl [iff]:
"x \<approx> x"
unfolding equiv_def by simp
--- a/src/HOL/List.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/List.thy Fri Oct 09 20:26:03 2015 +0200
@@ -80,15 +80,11 @@
syntax
-- \<open>Special syntax for filter\<close>
"_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
-
+syntax (xsymbols)
+ "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
translations
"[x<-xs . P]"== "CONST filter (%x. P) xs"
-syntax (xsymbols)
- "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
-syntax (HTML output)
- "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
-
primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
fold_Nil: "fold f [] = id" |
fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x"
@@ -421,8 +417,6 @@
syntax (xsymbols)
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
-syntax (HTML output)
- "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
parse_translation \<open>
let
--- a/src/HOL/NSA/HyperDef.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/NSA/HyperDef.thy Fri Oct 09 20:26:03 2015 +0200
@@ -34,10 +34,6 @@
omega ("\<omega>") and
epsilon ("\<epsilon>")
-notation (HTML output)
- omega ("\<omega>") and
- epsilon ("\<epsilon>")
-
subsection {* Real vector class instances *}
--- a/src/HOL/NSA/NSA.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/NSA/NSA.thy Fri Oct 09 20:26:03 2015 +0200
@@ -46,9 +46,6 @@
notation (xsymbols)
approx (infixl "\<approx>" 50)
-notation (HTML output)
- approx (infixl "\<approx>" 50)
-
lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}"
by (simp add: Reals_def image_def)
--- a/src/HOL/NanoJava/Equivalence.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy Fri Oct 09 20:26:03 2015 +0200
@@ -165,8 +165,6 @@
notation (xsymbols)
MGTe ("MGT\<^sub>e")
-notation (HTML output)
- MGTe ("MGT\<^sub>e")
lemma MGF_implies_complete:
"\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
--- a/src/HOL/Nat.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Nat.thy Fri Oct 09 20:26:03 2015 +0200
@@ -1317,9 +1317,6 @@
notation (latex output)
compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
-notation (HTML output)
- compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
-
text \<open>@{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f}\<close>
overloading
--- a/src/HOL/Orderings.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Orderings.thy Fri Oct 09 20:26:03 2015 +0200
@@ -102,10 +102,6 @@
less_eq ("op \<le>") and
less_eq ("(_/ \<le> _)" [51, 51] 50)
-notation (HTML output)
- less_eq ("op \<le>") and
- less_eq ("(_/ \<le> _)" [51, 51] 50)
-
abbreviation (input)
greater_eq (infix ">=" 50) where
"x >= y \<equiv> y <= x"
@@ -681,17 +677,6 @@
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)
-syntax (HTML output)
- "_All_less" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10)
- "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10)
- "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
- "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
-
- "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10)
- "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10)
- "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
- "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
-
translations
"ALL x<y. P" => "ALL x. x < y \<longrightarrow> P"
"EX x<y. P" => "EX x. x < y \<and> P"
--- a/src/HOL/Power.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Power.thy Fri Oct 09 20:26:03 2015 +0200
@@ -34,9 +34,6 @@
notation (latex output)
power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
-notation (HTML output)
- power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
-
text \<open>Special syntax for squares.\<close>
abbreviation (xsymbols)
@@ -46,9 +43,6 @@
notation (latex output)
power2 ("(_\<^sup>2)" [1000] 999)
-notation (HTML output)
- power2 ("(_\<^sup>2)" [1000] 999)
-
end
context monoid_mult
--- a/src/HOL/Probability/Fin_Map.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Probability/Fin_Map.thy Fri Oct 09 20:26:03 2015 +0200
@@ -102,13 +102,8 @@
syntax
"_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI' _:_./ _)" 10)
-
syntax (xsymbols)
"_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>' _\<in>_./ _)" 10)
-
-syntax (HTML output)
- "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>' _\<in>_./ _)" 10)
-
translations
"PI' x:A. B" == "CONST Pi' A (%x. B)"
@@ -616,13 +611,8 @@
syntax
"_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3PIF _:_./ _)" 10)
-
syntax (xsymbols)
"_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^sub>F _\<in>_./ _)" 10)
-
-syntax (HTML output)
- "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^sub>F _\<in>_./ _)" 10)
-
translations
"PIF x:I. M" == "CONST PiF I (%x. M)"
--- a/src/HOL/Probability/Finite_Product_Measure.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Fri Oct 09 20:26:03 2015 +0200
@@ -170,13 +170,8 @@
syntax
"_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3PIM _:_./ _)" 10)
-
syntax (xsymbols)
"_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^sub>M _\<in>_./ _)" 10)
-
-syntax (HTML output)
- "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^sub>M _\<in>_./ _)" 10)
-
translations
"PIM x:I. M" == "CONST PiM I (%x. M)"
--- a/src/HOL/Product_Type.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Product_Type.thy Fri Oct 09 20:26:03 2015 +0200
@@ -231,8 +231,6 @@
type_notation (xsymbols)
"prod" ("(_ \<times>/ _)" [21, 20] 20)
-type_notation (HTML output)
- "prod" ("(_ \<times>/ _)" [21, 20] 20)
definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
"Pair a b = Abs_prod (Pair_Rep a b)"
@@ -1009,9 +1007,6 @@
notation (xsymbols)
Times (infixr "\<times>" 80)
-notation (HTML output)
- Times (infixr "\<times>" 80)
-
hide_const (open) Times
syntax
--- a/src/HOL/Proofs/Lambda/LambdaType.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy Fri Oct 09 20:26:03 2015 +0200
@@ -17,9 +17,6 @@
notation (xsymbols)
shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
-notation (HTML output)
- shift ("_\<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)
--- a/src/HOL/Set.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Set.thy Fri Oct 09 20:26:03 2015 +0200
@@ -33,12 +33,6 @@
not_member ("op \<notin>") and
not_member ("(_/ \<notin> _)" [51, 51] 50)
-notation (HTML output)
- member ("op \<in>") and
- member ("(_/ \<in> _)" [51, 51] 50) and
- not_member ("op \<notin>") and
- not_member ("(_/ \<notin> _)" [51, 51] 50)
-
text \<open>Set comprehensions\<close>
@@ -167,12 +161,6 @@
subset_eq ("op \<subseteq>") and
subset_eq ("(_/ \<subseteq> _)" [51, 51] 50)
-notation (HTML output)
- subset ("op \<subset>") and
- subset ("(_/ \<subset> _)" [51, 51] 50) and
- subset_eq ("op \<subseteq>") and
- subset_eq ("(_/ \<subseteq> _)" [51, 51] 50)
-
abbreviation (input)
supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
"supset \<equiv> greater"
@@ -210,11 +198,6 @@
"_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
"_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
-syntax (HTML output)
- "_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)
- "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
-
translations
"ALL x:A. P" == "CONST Ball A (%x. P)"
"EX x:A. P" == "CONST Bex A (%x. P)"
@@ -242,13 +225,6 @@
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)
"_setleEx1" :: "[idt, 'a, bool] => bool" ("(3?! _<=_./ _)" [0, 0, 10] 10)
-syntax (HTML output)
- "_setlessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subset>_./ _)" [0, 0, 10] 10)
- "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subset>_./ _)" [0, 0, 10] 10)
- "_setleAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
- "_setleEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
- "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
-
translations
"\<forall>A\<subset>B. P" => "ALL A. A \<subset> B --> P"
"\<exists>A\<subset>B. P" => "EX A. A \<subset> B & P"
@@ -701,9 +677,6 @@
notation (xsymbols)
inter (infixl "\<inter>" 70)
-notation (HTML output)
- inter (infixl "\<inter>" 70)
-
lemma Int_def:
"A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
by (simp add: inf_set_def inf_fun_def)
@@ -735,9 +708,6 @@
notation (xsymbols)
union (infixl "\<union>" 65)
-notation (HTML output)
- union (infixl "\<union>" 65)
-
lemma Un_def:
"A \<union> B = {x. x \<in> A \<or> x \<in> B}"
by (simp add: sup_set_def sup_fun_def)
--- a/src/HOL/Set_Interval.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Set_Interval.thy Fri Oct 09 20:26:03 2015 +0200
@@ -1432,11 +1432,6 @@
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
-syntax (HTML output)
- "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
- "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
syntax (latex_sum output)
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
@@ -1783,11 +1778,6 @@
"_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
"_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
"_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
-syntax (HTML output)
- "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
- "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
syntax (latex_prod output)
"_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
--- a/src/HOL/Transitive_Closure.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Transitive_Closure.thy Fri Oct 09 20:26:03 2015 +0200
@@ -59,14 +59,6 @@
trancl ("(_\<^sup>+)" [1000] 999) and
reflcl ("(_\<^sup>=)" [1000] 999)
-notation (HTML output)
- rtranclp ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
- tranclp ("(_\<^sup>+\<^sup>+)" [1000] 1000) and
- reflclp ("(_\<^sup>=\<^sup>=)" [1000] 1000) and
- rtrancl ("(_\<^sup>*)" [1000] 999) and
- trancl ("(_\<^sup>+)" [1000] 999) and
- reflcl ("(_\<^sup>=)" [1000] 999)
-
subsection \<open>Reflexive closure\<close>
--- a/src/Sequents/LK0.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/Sequents/LK0.thy Fri Oct 09 20:26:03 2015 +0200
@@ -51,14 +51,6 @@
Ex (binder "\<exists>" 10) and
not_equal (infixl "\<noteq>" 50)
-notation (HTML output)
- Not ("\<not> _" [40] 40) and
- conj (infixr "\<and>" 35) and
- disj (infixr "\<or>" 30) and
- All (binder "\<forall>" 10) and
- Ex (binder "\<exists>" 10) and
- not_equal (infixl "\<noteq>" 50)
-
axiomatization where
(*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
--- a/src/ZF/Arith.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/Arith.thy Fri Oct 09 20:26:03 2015 +0200
@@ -75,9 +75,6 @@
notation (xsymbols)
mult (infixr "#\<times>" 70)
-notation (HTML output)
- mult (infixr "#\<times>" 70)
-
declare rec_type [simp]
nat_0_le [simp]
--- a/src/ZF/Cardinal.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/Cardinal.thy Fri Oct 09 20:26:03 2015 +0200
@@ -42,10 +42,6 @@
lesspoll (infixl "\<prec>" 50) and
Least (binder "\<mu>" 10)
-notation (HTML)
- eqpoll (infixl "\<approx>" 50) and
- Least (binder "\<mu>" 10)
-
subsection\<open>The Schroeder-Bernstein Theorem\<close>
text\<open>See Davey and Priestly, page 106\<close>
--- a/src/ZF/CardinalArith.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/CardinalArith.thy Fri Oct 09 20:26:03 2015 +0200
@@ -43,10 +43,6 @@
cadd (infixl "\<oplus>" 65) and
cmult (infixl "\<otimes>" 70)
-notation (HTML)
- cadd (infixl "\<oplus>" 65) and
- cmult (infixl "\<otimes>" 70)
-
lemma Card_Union [simp,intro,TC]:
assumes A: "\<And>x. x\<in>A \<Longrightarrow> Card(x)" shows "Card(\<Union>(A))"
--- a/src/ZF/Int_ZF.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/Int_ZF.thy Fri Oct 09 20:26:03 2015 +0200
@@ -95,10 +95,6 @@
zmult (infixl "$\<times>" 70) and
zle (infixl "$\<le>" 50) --\<open>less than or equals\<close>
-notation (HTML output)
- zmult (infixl "$\<times>" 70) and
- zle (infixl "$\<le>" 50)
-
declare quotientE [elim!]
--- a/src/ZF/Main_ZF.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/Main_ZF.thy Fri Oct 09 20:26:03 2015 +0200
@@ -19,8 +19,6 @@
notation (xsymbols)
iterates_omega ("(_^\<omega> '(_'))" [60,1000] 60)
-notation (HTML output)
- iterates_omega ("(_^\<omega> '(_'))" [60,1000] 60)
lemma iterates_triv:
"[| n\<in>nat; F(x) = x |] ==> F^n (x) = x"
--- a/src/ZF/OrdQuant.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/OrdQuant.thy Fri Oct 09 20:26:03 2015 +0200
@@ -36,10 +36,6 @@
"_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 \<open>simplification of the new quantifiers\<close>
@@ -208,9 +204,6 @@
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" == "CONST rall(M, %x. P)"
--- a/src/ZF/OrderType.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/OrderType.thy Fri Oct 09 20:26:03 2015 +0200
@@ -52,9 +52,6 @@
notation (xsymbols)
omult (infixl "\<times>\<times>" 70)
-notation (HTML output)
- omult (infixl "\<times>\<times>" 70)
-
subsection\<open>Proofs needing the combination of Ordinal.thy and Order.thy\<close>
--- a/src/ZF/Ordinal.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/Ordinal.thy Fri Oct 09 20:26:03 2015 +0200
@@ -34,9 +34,6 @@
notation (xsymbols)
le (infixl "\<le>" 50)
-notation (HTML output)
- le (infixl "\<le>" 50)
-
subsection\<open>Rules for Transset\<close>
--- a/src/ZF/ZF.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/ZF.thy Fri Oct 09 20:26:03 2015 +0200
@@ -171,31 +171,6 @@
"_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
"_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
-notation (HTML output)
- cart_prod (infixr "\<times>" 80) and
- Int (infixl "\<inter>" 70) and
- Un (infixl "\<union>" 65) and
- Subset (infixl "\<subseteq>" 50) and
- mem (infixl "\<in>" 50) and
- not_mem (infixl "\<notin>" 50) and
- Union ("\<Union>_" [90] 90) and
- Inter ("\<Inter>_" [90] 90)
-
-syntax (HTML output)
- "_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)
- "_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>")
-
-
defs (* Bounded Quantifiers *)
Ball_def: "Ball(A, P) == \<forall>x. x\<in>A \<longrightarrow> P(x)"
Bex_def: "Bex(A, P) == \<exists>x. x\<in>A & P(x)"