equal
deleted
inserted
replaced
42 generalizes the existing ``theorem (in ...)'' towards more versatility |
42 generalizes the existing ``theorem (in ...)'' towards more versatility |
43 and scalability. |
43 and scalability. |
44 |
44 |
45 |
45 |
46 *** Document preparation *** |
46 *** Document preparation *** |
|
47 |
|
48 * Added antiquotation @{theory thyname} which checks the given |
|
49 source text as name of a theory loaded or loadable via the current |
|
50 theory loader path. |
47 |
51 |
48 * Added antiquotations @{ML_type text} and @{ML_struct text} which |
52 * Added antiquotations @{ML_type text} and @{ML_struct text} which |
49 check the given source text as ML type/structure, printing verbatim. |
53 check the given source text as ML type/structure, printing verbatim. |
50 |
54 |
51 |
55 |
1618 theories. |
1622 theories. |
1619 |
1623 |
1620 |
1624 |
1621 *** ML *** |
1625 *** ML *** |
1622 |
1626 |
|
1627 * Pure/library.ML: added ##>, ##>>, #>> -- higher-order counterparts |
|
1628 for ||>, ||>>, |>>, |
|
1629 |
1623 * Pure/library.ML no longer defines its own option datatype, but uses |
1630 * Pure/library.ML no longer defines its own option datatype, but uses |
1624 that of the SML basis, which has constructors NONE and SOME instead of |
1631 that of the SML basis, which has constructors NONE and SOME instead of |
1625 None and Some, as well as exception Option.Option instead of OPTION. |
1632 None and Some, as well as exception Option.Option instead of OPTION. |
1626 The functions the, if_none, is_some, is_none have been adapted |
1633 The functions the, if_none, is_some, is_none have been adapted |
1627 accordingly, while Option.map replaces apsome. |
1634 accordingly, while Option.map replaces apsome. |