52 not_equal (infixl "\<noteq>" 50) |
52 not_equal (infixl "\<noteq>" 50) |
53 |
53 |
54 notation (HTML output) |
54 notation (HTML output) |
55 not_equal (infixl "\<noteq>" 50) |
55 not_equal (infixl "\<noteq>" 50) |
56 |
56 |
57 syntax (xsymbols) |
57 notation (xsymbols) |
58 Not :: "o => o" ("\<not> _" [40] 40) |
58 Not ("\<not> _" [40] 40) and |
59 "op &" :: "[o, o] => o" (infixr "\<and>" 35) |
59 "op &" (infixr "\<and>" 35) and |
60 "op |" :: "[o, o] => o" (infixr "\<or>" 30) |
60 "op |" (infixr "\<or>" 30) and |
61 "ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) |
61 All (binder "\<forall>" 10) and |
62 "EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) |
62 Ex (binder "\<exists>" 10) and |
63 "EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10) |
63 Ex1 (binder "\<exists>!" 10) and |
64 "op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) |
64 "op -->" (infixr "\<longrightarrow>" 25) and |
65 "op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) |
65 "op <->" (infixr "\<longleftrightarrow>" 25) |
66 |
66 |
67 syntax (HTML output) |
67 notation (HTML output) |
68 Not :: "o => o" ("\<not> _" [40] 40) |
68 Not ("\<not> _" [40] 40) and |
69 "op &" :: "[o, o] => o" (infixr "\<and>" 35) |
69 "op &" (infixr "\<and>" 35) and |
70 "op |" :: "[o, o] => o" (infixr "\<or>" 30) |
70 "op |" (infixr "\<or>" 30) and |
71 "ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) |
71 All (binder "\<forall>" 10) and |
72 "EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) |
72 Ex (binder "\<exists>" 10) and |
73 "EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10) |
73 Ex1 (binder "\<exists>!" 10) |
74 |
|
75 |
74 |
76 local |
75 local |
77 |
76 |
78 finalconsts |
77 finalconsts |
79 False All Ex |
78 False All Ex |