equal
deleted
inserted
replaced
54 translation. INCOMPATIBILITY -- use dummy abstraction instead, for |
54 translation. INCOMPATIBILITY -- use dummy abstraction instead, for |
55 example "A -> B" => "Pi A (%_. B)". |
55 example "A -> B" => "Pi A (%_. B)". |
56 |
56 |
57 |
57 |
58 *** HOL *** |
58 *** HOL *** |
|
59 |
|
60 * Alternative iff syntax "A <-> B" for equality on bool (with priority |
|
61 25 like -->); output depends on the "iff" print_mode, the default is |
|
62 "A = B" (with priority 50). |
59 |
63 |
60 * In the context of the assumption "~(s = t)" the Simplifier rewrites |
64 * In the context of the assumption "~(s = t)" the Simplifier rewrites |
61 "t = s" to False (by simproc "neq_simproc"). For backward |
65 "t = s" to False (by simproc "neq_simproc"). For backward |
62 compatibility this can be disabled by ML "reset use_neq_simproc". |
66 compatibility this can be disabled by ML "reset use_neq_simproc". |
63 |
67 |