# HG changeset patch # User wenzelm # Date 1444415163 -7200 # Node ID 3e04c9ca001a6db3f1f6044b58d4693c1c60ecca # Parent 517feb558c77bb88dbff54d413c965a2a4962677 discontinued specific HTML syntax; diff -r 517feb558c77 -r 3e04c9ca001a src/CTT/Arith.thy --- 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 "#\" 70) -notation (HTML output) - mult (infixr "#\" 70) - lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def diff -r 517feb558c77 -r 3e04c9ca001a src/CTT/CTT.thy --- 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 "\" 30) and Times (infixr "\" 50) -notation (HTML output) - lambda (binder "\\" 10) and - Elem ("(_ /\ _)" [10,10] 5) and - Eqelem ("(2_ =/ _ \/ _)" [10,10,10] 5) and - Times (infixr "\" 50) - syntax (xsymbols) "_PROD" :: "[idt,t,t] \ t" ("(3\ _\_./ _)" 10) "_SUM" :: "[idt,t,t] \ t" ("(3\ _\_./ _)" 10) -syntax (HTML output) - "_PROD" :: "[idt,t,t] \ t" ("(3\ _\_./ _)" 10) - "_SUM" :: "[idt,t,t] \ t" ("(3\ _\_./ _)" 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.*) diff -r 517feb558c77 -r 3e04c9ca001a src/FOL/IFOL.thy --- 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 "\" 50) - -notation (HTML output) - not_equal (infixl "\" 50) - -notation (xsymbols) + not_equal (infixl "\" 50) and Not ("\ _" [40] 40) and conj (infixr "\" 35) and disj (infixr "\" 30) and @@ -111,14 +106,6 @@ imp (infixr "\" 25) and iff (infixr "\" 25) -notation (HTML output) - Not ("\ _" [40] 40) and - conj (infixr "\" 35) and - disj (infixr "\" 30) and - All (binder "\" 10) and - Ex (binder "\" 10) and - Ex1 (binder "\!" 10) - subsection \Lemmas and proof tools\ diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Archimedean_Field.thy --- 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 ("\_\") -notation (HTML output) - floor ("\_\") - lemma floor_unique: "\of_int z \ x; x < of_int z + 1\ \ floor x = z" using floor_correct [of x] floor_exists1 [of x] by auto @@ -383,9 +380,6 @@ notation (xsymbols) ceiling ("\_\") -notation (HTML output) - ceiling ("\_\") - lemma ceiling_correct: "of_int (ceiling x) - 1 < x \ x \ of_int (ceiling x)" unfolding ceiling_def using floor_correct [of "- x"] by simp diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Filter.thy --- 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 "\\<^sub>\" 10) and Alm_all (binder "\\<^sub>\" 10) -notation (HTML output) - Inf_many (binder "\\<^sub>\" 10) and - Alm_all (binder "\\<^sub>\" 10) - lemma eventually_cofinite: "eventually P cofinite \ finite {x. \ P x}" unfolding cofinite_def proof (rule eventually_Abs_filter, rule is_filter.intro) diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Fun.thy --- 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 "\" 55) -notation (HTML output) - comp (infixl "\" 55) - lemma comp_apply [simp]: "(f o g) x = f (g x)" by (simp add: comp_def) diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Groups.thy --- 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 ("\_\") -notation (HTML output) - abs ("\_\") - end class sgn = diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Groups_Big.thy --- 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\_\_./ _)" [0, 51, 10] 10) -syntax (HTML output) - "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(2\_\_./ _)" [0, 51, 10] 10) translations -- \Beware of argument permutation!\ "SUM i:A. b" == "CONST setsum (%i. b) A" @@ -507,8 +505,6 @@ "_qsetsum" :: "pttrn \ bool \ 'a \ 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10) syntax (xsymbols) "_qsetsum" :: "pttrn \ bool \ 'a \ 'a" ("(2\_ | (_)./ _)" [0,0,10] 10) -syntax (HTML output) - "_qsetsum" :: "pttrn \ bool \ 'a \ 'a" ("(2\_ | (_)./ _)" [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\_\_./ _)" [0, 51, 10] 10) -syntax (HTML output) - "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\_\_./ _)" [0, 51, 10] 10) translations -- \Beware of argument permutation!\ "PROD i:A. b" == "CONST setprod (%i. b) A" @@ -1091,8 +1085,6 @@ "_qsetprod" :: "pttrn \ bool \ 'a \ 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10) syntax (xsymbols) "_qsetprod" :: "pttrn \ bool \ 'a \ 'a" ("(2\_ | (_)./ _)" [0,0,10] 10) -syntax (HTML output) - "_qsetprod" :: "pttrn \ bool \ 'a \ 'a" ("(2\_ | (_)./ _)" [0,0,10] 10) translations "PROD x|P. t" => "CONST setprod (%x. t) {x. P}" diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Groups_List.thy --- 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\_\_. _)" [0, 51, 10] 10) -syntax (HTML output) - "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) translations -- \Beware of argument permutation!\ "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\_\_. _)" [0, 51, 10] 10) -syntax (HTML output) - "_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10) translations -- \Beware of argument permutation!\ "PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)" diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/HOL.thy --- 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 "\" 50) -notation (HTML output) - Not ("\ _" [40] 40) and - conj (infixr "\" 35) and - disj (infixr "\" 30) and - not_equal (infix "\" 50) - abbreviation (iff) iff :: "[bool, bool] \ bool" (infixr "<->" 25) where "A <-> B \ A = B" @@ -154,11 +148,6 @@ Ex (binder "\" 10) and Ex1 (binder "\!" 10) -notation (HTML output) - All (binder "\" 10) and - Ex (binder "\" 10) and - Ex1 (binder "\!" 10) - notation (HOL) All (binder "! " 10) and Ex (binder "? " 10) and diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/HOLCF/Cfun.thy --- 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 ("(_\/_)" [999,1000] 999) -notation (HTML output) - Rep_cfun ("(_\/_)" [999,1000] 999) subsection {* Syntax for continuous lambda abstraction *} diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/HOLCF/IOA/meta_theory/Pred.thy --- 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 ("_ \ _" [100,9] 8) -notation (HTML output) - NOT ("\ _" [40] 40) and - AND (infixr "\" 35) and - OR (infixr "\" 30) - defs diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/HOLCF/Sprod.thy --- 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 ("(_ \/ _)" [21,20] 20) -type_notation (HTML output) - sprod ("(_ \/ _)" [21,20] 20) + subsection {* Definitions of constants *} diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/HOLCF/Ssum.thy --- 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 ("(_ \/ _)" [21, 20] 20) -type_notation (HTML output) - ssum ("(_ \/ _)" [21, 20] 20) subsection {* Definitions of constructors *} diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Library/Extended_Nat.thy --- 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 ("\") -notation (HTML output) - infinity ("\") subsection \Type definition\ diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Library/FuncSet.thy --- 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 \ 'a set \ 'b set \ ('a \ 'b) set" ("(3\ _\_./ _)" 10) "_lam" :: "pttrn \ 'a set \ ('a \ 'b) \ ('a \ 'b)" ("(3\_\_./ _)" [0,0,3] 3) -syntax (HTML output) - "_Pi" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3\ _\_./ _)" 10) - "_lam" :: "pttrn \ 'a set \ ('a \ 'b) \ ('a \ 'b)" ("(3\_\_./ _)" [0,0,3] 3) translations "\ x\A. B" \ "CONST Pi A (\x. B)" "\x\A. f" \ "CONST restrict (\x. f) A" @@ -357,8 +354,6 @@ "_PiE" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3PIE _:_./ _)" 10) syntax (xsymbols) "_PiE" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3\\<^sub>E _\_./ _)" 10) -syntax (HTML output) - "_PiE" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" ("(3\\<^sub>E _\_./ _)" 10) translations "\\<^sub>E x\A. B" \ "CONST Pi\<^sub>E A (\x. B)" abbreviation extensional_funcset :: "'a set \ 'b set \ ('a \ 'b) set" (infixr "->\<^sub>E" 60) diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Library/Groups_Big_Fun.thy --- 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 \ 'a \ 'a::comm_monoid_add" ("(3SUM _. _)" [0, 10] 10) syntax (xsymbols) "_Sum_any" :: "pttrn \ 'a \ 'a::comm_monoid_add" ("(3\_. _)" [0, 10] 10) -syntax (HTML output) - "_Sum_any" :: "pttrn \ 'a \ 'a::comm_monoid_add" ("(3\_. _)" [0, 10] 10) - translations "\a. b" == "CONST Sum_any (\a. b)" @@ -318,9 +315,6 @@ "_Prod_any" :: "pttrn \ 'a \ 'a::comm_monoid_mult" ("(3PROD _. _)" [0, 10] 10) syntax (xsymbols) "_Prod_any" :: "pttrn \ 'a \ 'a::comm_monoid_mult" ("(3\_. _)" [0, 10] 10) -syntax (HTML output) - "_Prod_any" :: "pttrn \ 'a \ 'a::comm_monoid_mult" ("(3\_. _)" [0, 10] 10) - translations "\a. b" == "CONST Prod_any (\a. b)" diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Library/Multiset.thy --- 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 \ 'b set \ 'a \ 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10) - syntax (xsymbols) "_msetsum_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" ("(3\_\#_. _)" [0, 51, 10] 10) - -syntax (HTML output) - "_msetsum_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" - ("(3\_\#_. _)" [0, 51, 10] 10) - translations "SUM i :# A. b" == "CONST msetsum (CONST image_mset (\i. b) A)" @@ -1322,15 +1316,9 @@ syntax "_msetprod_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_mult" ("(3PROD _:#_. _)" [0, 51, 10] 10) - syntax (xsymbols) "_msetprod_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_mult" ("(3\_\#_. _)" [0, 51, 10] 10) - -syntax (HTML output) - "_msetprod_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_mult" - ("(3\_\#_. _)" [0, 51, 10] 10) - translations "PROD i :# A. b" == "CONST msetprod (CONST image_mset (\i. b) A)" diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Library/Preorder.thy --- 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 \") and equiv ("(_/ \ _)" [51, 51] 50) -notation (HTML output) - equiv ("op \") and - equiv ("(_/ \ _)" [51, 51] 50) - lemma refl [iff]: "x \ x" unfolding equiv_def by simp diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/List.thy --- 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 -- \Special syntax for filter\ "_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])") - +syntax (xsymbols) + "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])") translations "[x<-xs . P]"== "CONST filter (%x. P) xs" -syntax (xsymbols) - "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])") -syntax (HTML output) - "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])") - primrec fold :: "('a \ 'b \ 'b) \ 'a list \ 'b \ 'b" where fold_Nil: "fold f [] = id" | fold_Cons: "fold f (x # xs) = fold f xs \ f x" @@ -421,8 +417,6 @@ syntax (xsymbols) "_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ \ _") -syntax (HTML output) - "_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ \ _") parse_translation \ let diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/NSA/HyperDef.thy --- 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 ("\") and epsilon ("\") -notation (HTML output) - omega ("\") and - epsilon ("\") - subsection {* Real vector class instances *} diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/NSA/NSA.thy --- 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 "\" 50) -notation (HTML output) - approx (infixl "\" 50) - lemma SReal_def: "\ == {x. \r. x = hypreal_of_real r}" by (simp add: Reals_def image_def) diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/NanoJava/Equivalence.thy --- 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: "\Z. {} |\ { MGT c Z} \ \ {P} c {Q} \ {} \ {P} c {Q}" diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Nat.thy --- 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 \@{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f}\ overloading diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Orderings.thy --- 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 \") and less_eq ("(_/ \ _)" [51, 51] 50) -notation (HTML output) - less_eq ("op \") and - less_eq ("(_/ \ _)" [51, 51] 50) - abbreviation (input) greater_eq (infix ">=" 50) where "x >= y \ 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\_<_./ _)" [0, 0, 10] 10) - "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\_<_./ _)" [0, 0, 10] 10) - "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) - "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) - - "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) - "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\_>_./ _)" [0, 0, 10] 10) - "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) - "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) - translations "ALL x "ALL x. x < y \ P" "EX x "EX x. x < y \ P" diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Power.thy --- 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 \Special syntax for squares.\ 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 diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Probability/Fin_Map.thy --- 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\' _\_./ _)" 10) - -syntax (HTML output) - "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\' _\_./ _)" 10) - translations "PI' x:A. B" == "CONST Pi' A (%x. B)" @@ -616,13 +611,8 @@ syntax "_PiF" :: "pttrn \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3PIF _:_./ _)" 10) - syntax (xsymbols) "_PiF" :: "pttrn \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3\\<^sub>F _\_./ _)" 10) - -syntax (HTML output) - "_PiF" :: "pttrn \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3\\<^sub>F _\_./ _)" 10) - translations "PIF x:I. M" == "CONST PiF I (%x. M)" diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Probability/Finite_Product_Measure.thy --- 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 \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3PIM _:_./ _)" 10) - syntax (xsymbols) "_PiM" :: "pttrn \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3\\<^sub>M _\_./ _)" 10) - -syntax (HTML output) - "_PiM" :: "pttrn \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3\\<^sub>M _\_./ _)" 10) - translations "PIM x:I. M" == "CONST PiM I (%x. M)" diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Product_Type.thy --- 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" ("(_ \/ _)" [21, 20] 20) -type_notation (HTML output) - "prod" ("(_ \/ _)" [21, 20] 20) definition Pair :: "'a \ 'b \ 'a \ 'b" where "Pair a b = Abs_prod (Pair_Rep a b)" @@ -1009,9 +1007,6 @@ notation (xsymbols) Times (infixr "\" 80) -notation (HTML output) - Times (infixr "\" 80) - hide_const (open) Times syntax diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Proofs/Lambda/LambdaType.thy --- 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 ("_\_:_\" [90, 0, 0] 91) -notation (HTML output) - shift ("_\_:_\" [90, 0, 0] 91) - lemma shift_eq [simp]: "i = j \ (e\i:T\) j = T" by (simp add: shift_def) diff -r 517feb558c77 -r 3e04c9ca001a src/HOL/Set.thy --- 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 \") and not_member ("(_/ \ _)" [51, 51] 50) -notation (HTML output) - member ("op \") and - member ("(_/ \ _)" [51, 51] 50) and - not_member ("op \") and - not_member ("(_/ \ _)" [51, 51] 50) - text \Set comprehensions\ @@ -167,12 +161,6 @@ subset_eq ("op \") and subset_eq ("(_/ \ _)" [51, 51] 50) -notation (HTML output) - subset ("op \") and - subset ("(_/ \ _)" [51, 51] 50) and - subset_eq ("op \") and - subset_eq ("(_/ \ _)" [51, 51] 50) - abbreviation (input) supset :: "'a set \ 'a set \ bool" where "supset \ greater" @@ -210,11 +198,6 @@ "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\!_\_./ _)" [0, 0, 10] 10) "_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST_\_./ _)" [0, 0, 10] 10) -syntax (HTML output) - "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\_\_./ _)" [0, 0, 10] 10) - "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\_\_./ _)" [0, 0, 10] 10) - "_Bex1" :: "pttrn => 'a set => bool => bool" ("(3\!_\_./ _)" [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\_\_./ _)" [0, 0, 10] 10) - "_setlessEx" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) - "_setleAll" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) - "_setleEx" :: "[idt, 'a, bool] => bool" ("(3\_\_./ _)" [0, 0, 10] 10) - "_setleEx1" :: "[idt, 'a, bool] => bool" ("(3\!_\_./ _)" [0, 0, 10] 10) - translations "\A\B. P" => "ALL A. A \ B --> P" "\A\B. P" => "EX A. A \ B & P" @@ -701,9 +677,6 @@ notation (xsymbols) inter (infixl "\" 70) -notation (HTML output) - inter (infixl "\" 70) - lemma Int_def: "A \ B = {x. x \ A \ x \ B}" by (simp add: inf_set_def inf_fun_def) @@ -735,9 +708,6 @@ notation (xsymbols) union (infixl "\" 65) -notation (HTML output) - union (infixl "\" 65) - lemma Un_def: "A \