equal
deleted
inserted
replaced
515 powerful on arithmetic goals. |
515 powerful on arithmetic goals. |
516 INCOMPATIBILTY: rewrite proofs. Set fast_arith_split_limit to 0 to obtain |
516 INCOMPATIBILTY: rewrite proofs. Set fast_arith_split_limit to 0 to obtain |
517 the old behavior. |
517 the old behavior. |
518 |
518 |
519 * Support for hex (0x20) and binary (0b1001) numerals. |
519 * Support for hex (0x20) and binary (0b1001) numerals. |
|
520 |
|
521 * New method: |
|
522 reify eqs (t), where eqs are equations for an interpretation |
|
523 I :: 'a list => 'b => 'c and t::'c is an optional parameter, |
|
524 computes a term s::'b and a list xs::'a list and proves the theorem |
|
525 I xs s = t. This is also known as reification or quoting. The resulting theorem is applied to the subgoal to substitute t with I xs s. |
|
526 If t is omitted, the subgoal itself is reified. |
|
527 |
|
528 * New method: |
|
529 reflection corr_thm eqs (t). The parameters eqs and (t) are as explained above. corr_thm is a theorem for |
|
530 I vs (f t) = I vs t, where f is supposed to be a computable function (in the sense of code generattion). The method uses reify to compute s and xs as above then applies corr_thm and uses normalization by evaluation to "prove" f s = r and finally gets the theorem t = r, which is again applied to the subgoal. An Example is available in HOL/ex/ReflectionEx.thy. |
520 |
531 |
521 *** HOL-Algebra *** |
532 *** HOL-Algebra *** |
522 |
533 |
523 * Method algebra is now set up via an attribute. For examples see CRing.thy. |
534 * Method algebra is now set up via an attribute. For examples see CRing.thy. |
524 INCOMPATIBILITY: the method is now weaker on combinations of algebraic |
535 INCOMPATIBILITY: the method is now weaker on combinations of algebraic |