src/HOL/HOL.thy
changeset 50360 628b37b9e8a2
parent 49339 d1fcb4de8349
child 51021 1cf4faed8b22
equal deleted inserted replaced
50354:4a955d23c79b 50360:628b37b9e8a2
    93 notation (xsymbols)
    93 notation (xsymbols)
    94   Not  ("\<not> _" [40] 40) and
    94   Not  ("\<not> _" [40] 40) and
    95   conj  (infixr "\<and>" 35) and
    95   conj  (infixr "\<and>" 35) and
    96   disj  (infixr "\<or>" 30) and
    96   disj  (infixr "\<or>" 30) and
    97   implies  (infixr "\<longrightarrow>" 25) and
    97   implies  (infixr "\<longrightarrow>" 25) and
       
    98   not_equal  (infixl "\<noteq>" 50)
       
    99 
       
   100 notation (xsymbols output)
    98   not_equal  (infix "\<noteq>" 50)
   101   not_equal  (infix "\<noteq>" 50)
    99 
   102 
   100 notation (HTML output)
   103 notation (HTML output)
   101   Not  ("\<not> _" [40] 40) and
   104   Not  ("\<not> _" [40] 40) and
   102   conj  (infixr "\<and>" 35) and
   105   conj  (infixr "\<and>" 35) and