src/HOL/HOL.thy
changeset 61378 3e04c9ca001a
parent 61222 05d28dc76e5c
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/HOL.thy	Fri Oct 09 19:51:20 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Oct 09 20:26:03 2015 +0200
     1.3 @@ -112,12 +112,6 @@
     1.4  notation (xsymbols output)
     1.5    not_equal  (infix "\<noteq>" 50)
     1.6  
     1.7 -notation (HTML output)
     1.8 -  Not  ("\<not> _" [40] 40) and
     1.9 -  conj  (infixr "\<and>" 35) and
    1.10 -  disj  (infixr "\<or>" 30) and
    1.11 -  not_equal  (infix "\<noteq>" 50)
    1.12 -
    1.13  abbreviation (iff)
    1.14    iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "<->" 25) where
    1.15    "A <-> B \<equiv> A = B"
    1.16 @@ -154,11 +148,6 @@
    1.17    Ex  (binder "\<exists>" 10) and
    1.18    Ex1  (binder "\<exists>!" 10)
    1.19  
    1.20 -notation (HTML output)
    1.21 -  All  (binder "\<forall>" 10) and
    1.22 -  Ex  (binder "\<exists>" 10) and
    1.23 -  Ex1  (binder "\<exists>!" 10)
    1.24 -
    1.25  notation (HOL)
    1.26    All  (binder "! " 10) and
    1.27    Ex  (binder "? " 10) and