equal
deleted
inserted
replaced
507 association lists. |
507 association lists. |
508 |
508 |
509 * New proof method "evaluation" for efficiently solving a goal |
509 * New proof method "evaluation" for efficiently solving a goal |
510 (i.e. a boolean expression) by compiling it to ML. The goal is |
510 (i.e. a boolean expression) by compiling it to ML. The goal is |
511 "proved" (via the oracle "Evaluation") if it evaluates to True. |
511 "proved" (via the oracle "Evaluation") if it evaluates to True. |
|
512 |
|
513 * Linear arithmetic now splits certain operators (e.g. min, max, abs) also |
|
514 when invoked by the simplifier. This results in the simplifier being more |
|
515 powerful on arithmetic goals. |
|
516 INCOMPATIBILTY: rewrite proofs. Set fast_arith_split_limit to 0 to obtain |
|
517 the old behavior. |
512 |
518 |
513 * Support for hex (0x20) and binary (0b1001) numerals. |
519 * Support for hex (0x20) and binary (0b1001) numerals. |
514 |
520 |
515 *** HOL-Algebra *** |
521 *** HOL-Algebra *** |
516 |
522 |