equal
deleted
inserted
replaced
12 term < logic |
12 term < logic |
13 plus < term |
13 plus < term |
14 minus < term |
14 minus < term |
15 times < term |
15 times < term |
16 |
16 |
17 default term |
17 default |
|
18 term |
18 |
19 |
19 types |
20 types |
20 bool 0 |
21 bool 0 |
21 |
22 |
22 arities |
23 arities |
51 "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10) |
52 "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10) |
52 |
53 |
53 (* Infixes *) |
54 (* Infixes *) |
54 |
55 |
55 o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) |
56 o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) |
56 "=", "~=" :: "['a, 'a] => bool" (infixl 50) |
57 "=" :: "['a, 'a] => bool" (infixl 50) |
|
58 "~=" :: "['a, 'a] => bool" ("(_ ~=/ _)" [50, 51] 50) |
57 "&" :: "[bool, bool] => bool" (infixr 35) |
59 "&" :: "[bool, bool] => bool" (infixr 35) |
58 "|" :: "[bool, bool] => bool" (infixr 30) |
60 "|" :: "[bool, bool] => bool" (infixr 30) |
59 "-->" :: "[bool, bool] => bool" (infixr 25) |
61 "-->" :: "[bool, bool] => bool" (infixr 25) |
60 |
62 |
61 (* Overloaded Constants *) |
63 (* Overloaded Constants *) |
67 |
69 |
68 translations |
70 translations |
69 "ALL xs. P" => "! xs. P" |
71 "ALL xs. P" => "! xs. P" |
70 "EX xs. P" => "? xs. P" |
72 "EX xs. P" => "? xs. P" |
71 "EX! xs. P" => "?! xs. P" |
73 "EX! xs. P" => "?! xs. P" |
|
74 "x ~= y" == "~ (x = y)" |
|
75 "let x = s in t" == "Let(s, %x. t)" |
72 |
76 |
73 "x ~= y" == "~ (x=y)" |
|
74 "let x = s in t" == "Let(s, %x. t)" |
|
75 |
77 |
76 rules |
78 rules |
77 |
79 |
78 eq_reflection "(x=y) ==> (x==y)" |
80 eq_reflection "(x=y) ==> (x==y)" |
79 |
81 |