56 |
56 |
57 notation (output) |
57 notation (output) |
58 "op =" (infix "=" 50) |
58 "op =" (infix "=" 50) |
59 |
59 |
60 abbreviation |
60 abbreviation |
61 not_equal :: "['a, 'a] => bool" (infixl "~=" 50) |
61 not_equal :: "['a, 'a] => bool" (infixl "~=" 50) where |
62 "x ~= y == ~ (x = y)" |
62 "x ~= y == ~ (x = y)" |
63 |
63 |
64 notation (output) |
64 notation (output) |
65 not_equal (infix "~=" 50) |
65 not_equal (infix "~=" 50) |
66 |
66 |
67 notation (xsymbols) |
67 notation (xsymbols) |
68 Not ("\<not> _" [40] 40) |
68 Not ("\<not> _" [40] 40) and |
69 "op &" (infixr "\<and>" 35) |
69 "op &" (infixr "\<and>" 35) and |
70 "op |" (infixr "\<or>" 30) |
70 "op |" (infixr "\<or>" 30) and |
71 "op -->" (infixr "\<longrightarrow>" 25) |
71 "op -->" (infixr "\<longrightarrow>" 25) and |
72 not_equal (infix "\<noteq>" 50) |
72 not_equal (infix "\<noteq>" 50) |
73 |
73 |
74 notation (HTML output) |
74 notation (HTML output) |
75 Not ("\<not> _" [40] 40) |
75 Not ("\<not> _" [40] 40) and |
76 "op &" (infixr "\<and>" 35) |
76 "op &" (infixr "\<and>" 35) and |
77 "op |" (infixr "\<or>" 30) |
77 "op |" (infixr "\<or>" 30) and |
78 not_equal (infix "\<noteq>" 50) |
78 not_equal (infix "\<noteq>" 50) |
79 |
79 |
80 abbreviation (iff) |
80 abbreviation (iff) |
81 iff :: "[bool, bool] => bool" (infixr "<->" 25) |
81 iff :: "[bool, bool] => bool" (infixr "<->" 25) where |
82 "A <-> B == A = B" |
82 "A <-> B == A = B" |
83 |
83 |
84 notation (xsymbols) |
84 notation (xsymbols) |
85 iff (infixr "\<longleftrightarrow>" 25) |
85 iff (infixr "\<longleftrightarrow>" 25) |
86 |
86 |