45 syntax |
45 syntax |
46 "~=" :: "['a, 'a] => o" (infixl 50) |
46 "~=" :: "['a, 'a] => o" (infixl 50) |
47 translations |
47 translations |
48 "x ~= y" == "~ (x = y)" |
48 "x ~= y" == "~ (x = y)" |
49 |
49 |
50 syntax (symbols) |
50 syntax (xsymbols) |
51 Not :: "o => o" ("\<not> _" [40] 40) |
51 Not :: "o => o" ("\<not> _" [40] 40) |
52 "op &" :: "[o, o] => o" (infixr "\<and>" 35) |
52 "op &" :: "[o, o] => o" (infixr "\<and>" 35) |
53 "op |" :: "[o, o] => o" (infixr "\<or>" 30) |
53 "op |" :: "[o, o] => o" (infixr "\<or>" 30) |
54 "op -->" :: "[o, o] => o" (infixr "\<midarrow>\<rightarrow>" 25) |
|
55 "op <->" :: "[o, o] => o" (infixr "\<leftarrow>\<rightarrow>" 25) |
|
56 "ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) |
54 "ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) |
57 "EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) |
55 "EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) |
58 "EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10) |
56 "EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10) |
59 "op ~=" :: "['a, 'a] => o" (infixl "\<noteq>" 50) |
57 "op ~=" :: "['a, 'a] => o" (infixl "\<noteq>" 50) |
60 |
|
61 syntax (xsymbols) |
|
62 "op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) |
58 "op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) |
63 "op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) |
59 "op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) |
64 |
60 |
65 syntax (HTML output) |
61 syntax (HTML output) |
66 Not :: "o => o" ("\<not> _" [40] 40) |
62 Not :: "o => o" ("\<not> _" [40] 40) |