equal
deleted
inserted
replaced
253 i*j + k + j*#3*i simplifies to #4*(i*j) + k |
253 i*j + k + j*#3*i simplifies to #4*(i*j) + k |
254 two terms #m*u and #n*u are replaced by #(m+n)*u |
254 two terms #m*u and #n*u are replaced by #(m+n)*u |
255 (where #m, #n and u can implicitly be 1; this is simproc combine_numerals) |
255 (where #m, #n and u can implicitly be 1; this is simproc combine_numerals) |
256 and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y |
256 and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y |
257 or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals); |
257 or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals); |
|
258 |
|
259 * HOL: meson_tac is available (previously in ex/meson.ML). It is a powerful |
|
260 prover for predicate logic but knows nothing of clasets. For examples of |
|
261 what it can do, see ex/mesontest.ML and ex/mesontest2.ML; |
258 |
262 |
259 * HOL: new version of "case_tac" subsumes both boolean case split and |
263 * HOL: new version of "case_tac" subsumes both boolean case split and |
260 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer |
264 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer |
261 exists, may define val exhaust_tac = case_tac for ad-hoc portability; |
265 exists, may define val exhaust_tac = case_tac for ad-hoc portability; |
262 |
266 |