equal
deleted
inserted
replaced
624 feature is used only for decision, for compatibility with arith. This |
624 feature is used only for decision, for compatibility with arith. This |
625 means a goal is either solved or left unchanged, no simplification. |
625 means a goal is either solved or left unchanged, no simplification. |
626 |
626 |
627 |
627 |
628 *** ML *** |
628 *** ML *** |
|
629 |
|
630 * Pure/library: |
|
631 |
|
632 infixes ins ins_string ins_int have been abandoned in favour of insert. |
|
633 INCOMPATIBILITY: rewrite "x ins(_...) xs" to "insert (op =) x xs" |
629 |
634 |
630 * Pure/General/susp.ML: |
635 * Pure/General/susp.ML: |
631 |
636 |
632 New module for delayed evaluations. |
637 New module for delayed evaluations. |
633 |
638 |