src/HOL/HOL.thy
changeset 21404 eb85850d3eb7
parent 21250 a268f6288fb6
child 21410 c212b002fc8c
     1.1 --- a/src/HOL/HOL.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -58,27 +58,27 @@
     1.4    "op ="  (infix "=" 50)
     1.5  
     1.6  abbreviation
     1.7 -  not_equal     :: "['a, 'a] => bool"               (infixl "~=" 50)
     1.8 +  not_equal :: "['a, 'a] => bool"  (infixl "~=" 50) where
     1.9    "x ~= y == ~ (x = y)"
    1.10  
    1.11  notation (output)
    1.12    not_equal  (infix "~=" 50)
    1.13  
    1.14  notation (xsymbols)
    1.15 -  Not  ("\<not> _" [40] 40)
    1.16 -  "op &"  (infixr "\<and>" 35)
    1.17 -  "op |"  (infixr "\<or>" 30)
    1.18 -  "op -->"  (infixr "\<longrightarrow>" 25)
    1.19 +  Not  ("\<not> _" [40] 40) and
    1.20 +  "op &"  (infixr "\<and>" 35) and
    1.21 +  "op |"  (infixr "\<or>" 30) and
    1.22 +  "op -->"  (infixr "\<longrightarrow>" 25) and
    1.23    not_equal  (infix "\<noteq>" 50)
    1.24  
    1.25  notation (HTML output)
    1.26 -  Not  ("\<not> _" [40] 40)
    1.27 -  "op &"  (infixr "\<and>" 35)
    1.28 -  "op |"  (infixr "\<or>" 30)
    1.29 +  Not  ("\<not> _" [40] 40) and
    1.30 +  "op &"  (infixr "\<and>" 35) and
    1.31 +  "op |"  (infixr "\<or>" 30) and
    1.32    not_equal  (infix "\<noteq>" 50)
    1.33  
    1.34  abbreviation (iff)
    1.35 -  iff :: "[bool, bool] => bool"  (infixr "<->" 25)
    1.36 +  iff :: "[bool, bool] => bool"  (infixr "<->" 25) where
    1.37    "A <-> B == A = B"
    1.38  
    1.39  notation (xsymbols)