equal
deleted
inserted
replaced
5 |
5 |
6 Intuitionistic first-order logic. |
6 Intuitionistic first-order logic. |
7 *) |
7 *) |
8 |
8 |
9 IFOL = Pure + |
9 IFOL = Pure + |
|
10 |
|
11 global |
10 |
12 |
11 classes |
13 classes |
12 term < logic |
14 term < logic |
13 |
15 |
14 default |
16 default |
60 "EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10) |
62 "EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10) |
61 "EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10) |
63 "EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10) |
62 "op ~=" :: ['a, 'a] => o (infixl "\\<noteq>" 50) |
64 "op ~=" :: ['a, 'a] => o (infixl "\\<noteq>" 50) |
63 |
65 |
64 |
66 |
|
67 path IFOL |
|
68 |
65 rules |
69 rules |
66 |
70 |
67 (* Equality *) |
71 (* Equality *) |
68 |
72 |
69 refl "a=a" |
73 refl "a=a" |
106 |
110 |
107 eq_reflection "(x=y) ==> (x==y)" |
111 eq_reflection "(x=y) ==> (x==y)" |
108 iff_reflection "(P<->Q) ==> (P==Q)" |
112 iff_reflection "(P<->Q) ==> (P==Q)" |
109 |
113 |
110 end |
114 end |
111 |
|