22 |
22 |
23 Trueprop :: "two_seqi" |
23 Trueprop :: "two_seqi" |
24 |
24 |
25 True :: o |
25 True :: o |
26 False :: o |
26 False :: o |
27 "=" :: "['a,'a] => o" (infixl 50) |
27 equal :: "['a,'a] => o" (infixl "=" 50) |
28 Not :: "o => o" ("~ _" [40] 40) |
28 Not :: "o => o" ("~ _" [40] 40) |
29 "&" :: "[o,o] => o" (infixr 35) |
29 conj :: "[o,o] => o" (infixr "&" 35) |
30 "|" :: "[o,o] => o" (infixr 30) |
30 disj :: "[o,o] => o" (infixr "|" 30) |
31 "-->" :: "[o,o] => o" (infixr 25) |
31 imp :: "[o,o] => o" (infixr "-->" 25) |
32 "<->" :: "[o,o] => o" (infixr 25) |
32 iff :: "[o,o] => o" (infixr "<->" 25) |
33 The :: "('a => o) => 'a" (binder "THE " 10) |
33 The :: "('a => o) => 'a" (binder "THE " 10) |
34 All :: "('a => o) => o" (binder "ALL " 10) |
34 All :: "('a => o) => o" (binder "ALL " 10) |
35 Ex :: "('a => o) => o" (binder "EX " 10) |
35 Ex :: "('a => o) => o" (binder "EX " 10) |
36 |
36 |
37 syntax |
37 syntax |
38 "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) |
38 "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) |
39 "_not_equal" :: "['a, 'a] => o" (infixl "~=" 50) |
|
40 |
39 |
41 parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *} |
40 parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *} |
42 print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *} |
41 print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *} |
43 |
42 |
44 translations |
43 abbreviation |
45 "x ~= y" == "~ (x = y)" |
44 not_equal (infixl "~=" 50) where |
|
45 "x ~= y == ~ (x = y)" |
46 |
46 |
47 syntax (xsymbols) |
47 syntax (xsymbols) |
48 Not :: "o => o" ("\<not> _" [40] 40) |
48 Not :: "o => o" ("\<not> _" [40] 40) |
49 "op &" :: "[o, o] => o" (infixr "\<and>" 35) |
49 conj :: "[o, o] => o" (infixr "\<and>" 35) |
50 "op |" :: "[o, o] => o" (infixr "\<or>" 30) |
50 disj :: "[o, o] => o" (infixr "\<or>" 30) |
51 "op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) |
51 imp :: "[o, o] => o" (infixr "\<longrightarrow>" 25) |
52 "op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) |
52 iff :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) |
53 All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) |
53 All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) |
54 Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) |
54 Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) |
55 "_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50) |
55 not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50) |
56 |
56 |
57 syntax (HTML output) |
57 syntax (HTML output) |
58 Not :: "o => o" ("\<not> _" [40] 40) |
58 Not :: "o => o" ("\<not> _" [40] 40) |
59 "op &" :: "[o, o] => o" (infixr "\<and>" 35) |
59 conj :: "[o, o] => o" (infixr "\<and>" 35) |
60 "op |" :: "[o, o] => o" (infixr "\<or>" 30) |
60 disj :: "[o, o] => o" (infixr "\<or>" 30) |
61 All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) |
61 All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) |
62 Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) |
62 Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) |
63 "_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50) |
63 not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50) |
64 |
64 |
65 local |
65 local |
66 |
66 |
67 axioms |
67 axioms |
68 |
68 |