equal
deleted
inserted
replaced
20 term |
20 term |
21 |
21 |
22 consts |
22 consts |
23 |
23 |
24 Trueprop :: "two_seqi" |
24 Trueprop :: "two_seqi" |
25 "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) |
|
26 |
25 |
27 True,False :: o |
26 True,False :: o |
28 "=" :: ['a,'a] => o (infixl 50) |
27 "=" :: ['a,'a] => o (infixl 50) |
29 Not :: o => o ("~ _" [40] 40) |
28 Not :: o => o ("~ _" [40] 40) |
30 "&" :: [o,o] => o (infixr 35) |
29 "&" :: [o,o] => o (infixr 35) |
33 The :: ('a => o) => 'a (binder "THE " 10) |
32 The :: ('a => o) => 'a (binder "THE " 10) |
34 All :: ('a => o) => o (binder "ALL " 10) |
33 All :: ('a => o) => o (binder "ALL " 10) |
35 Ex :: ('a => o) => o (binder "EX " 10) |
34 Ex :: ('a => o) => o (binder "EX " 10) |
36 |
35 |
37 syntax |
36 syntax |
|
37 "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) |
38 "_not_equal" :: ['a, 'a] => o (infixl "~=" 50) |
38 "_not_equal" :: ['a, 'a] => o (infixl "~=" 50) |
39 |
39 |
40 translations |
40 translations |
41 "x ~= y" == "~ (x = y)" |
41 "x ~= y" == "~ (x = y)" |
42 |
42 |