equal
deleted
inserted
replaced
622 solving continuity subgoals on terms with lambda abstractions. In |
622 solving continuity subgoals on terms with lambda abstractions. In |
623 some rare cases the new simproc may fail to solve subgoals that the |
623 some rare cases the new simproc may fail to solve subgoals that the |
624 old one could solve, and "simp add: cont2cont_LAM" may be necessary. |
624 old one could solve, and "simp add: cont2cont_LAM" may be necessary. |
625 Potential INCOMPATIBILITY. |
625 Potential INCOMPATIBILITY. |
626 |
626 |
627 * The syntax of the fixrec package now conforms to the general |
627 * Command 'fixrec': specification syntax now conforms to the general |
628 specification format of inductive, primrec, function, etc. See |
628 format as seen in 'inductive', 'primrec', 'function', etc. See |
629 src/HOLCF/ex/Fixrec_ex.thy for examples. INCOMPATIBILITY. |
629 src/HOLCF/ex/Fixrec_ex.thy for examples. INCOMPATIBILITY. |
630 |
630 |
631 |
631 |
632 *** ZF *** |
632 *** ZF *** |
633 |
633 |