equal
deleted
inserted
replaced
51 "EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10) |
51 "EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10) |
52 "_not_equal" :: ['a, 'a] => o (infixl "\\<noteq>" 50) |
52 "_not_equal" :: ['a, 'a] => o (infixl "\\<noteq>" 50) |
53 |
53 |
54 syntax (HTML output) |
54 syntax (HTML output) |
55 Not :: o => o ("\\<not> _" [40] 40) |
55 Not :: o => o ("\\<not> _" [40] 40) |
|
56 "op &" :: [o, o] => o (infixr "\\<and>" 35) |
|
57 "op |" :: [o, o] => o (infixr "\\<or>" 30) |
|
58 "ALL " :: [idts, o] => o ("(3\\<forall>_./ _)" [0, 10] 10) |
|
59 "EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10) |
|
60 "EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10) |
|
61 "_not_equal" :: ['a, 'a] => o (infixl "\\<noteq>" 50) |
56 |
62 |
57 |
63 |
58 local |
64 local |
59 |
65 |
60 rules |
66 rules |