equal
deleted
inserted
replaced
768 ML {* @{simpset} *} |
768 ML {* @{simpset} *} |
769 ML {* @{claset} *} |
769 ML {* @{claset} *} |
770 ML {* @{clasimpset} *} |
770 ML {* @{clasimpset} *} |
771 |
771 |
772 The same works for sources being ``used'' within an Isar context. |
772 The same works for sources being ``used'' within an Isar context. |
|
773 |
|
774 * ML in Isar: improved error reporting; extra verbosity with |
|
775 Toplevel.debug enabled. |
773 |
776 |
774 * Pure/library: |
777 * Pure/library: |
775 |
778 |
776 val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list |
779 val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list |
777 val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd |
780 val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd |