equal
deleted
inserted
replaced
547 feature is used only for decision, for compatibility with arith. This |
547 feature is used only for decision, for compatibility with arith. This |
548 means a goal is either solved or left unchanged, no simplification. |
548 means a goal is either solved or left unchanged, no simplification. |
549 |
549 |
550 |
550 |
551 *** ML *** |
551 *** ML *** |
|
552 |
|
553 * Pure/library: |
|
554 |
|
555 Semantically identical functions "equal_list" and "eq_list" have been |
|
556 unified to "eq_list". |
552 |
557 |
553 * Pure/library: |
558 * Pure/library: |
554 |
559 |
555 val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list |
560 val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list |
556 val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd |
561 val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd |