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