equal
deleted
inserted
replaced
43 and scalability. |
43 and scalability. |
44 |
44 |
45 |
45 |
46 *** Document preparation *** |
46 *** Document preparation *** |
47 |
47 |
48 * Added antiquotation @{theory name} which prints the name $A$, after |
48 * Added antiquotation @{theory name} which prints the given name, |
49 checking that it refers to a valid ancestor theory in the current |
49 after checking that it refers to a valid ancestor theory in the |
50 context. |
50 current context. |
51 |
51 |
52 * Added antiquotations @{ML_type text} and @{ML_struct text} which |
52 * Added antiquotations @{ML_type text} and @{ML_struct text} which |
53 check the given source text as ML type/structure, printing verbatim. |
53 check the given source text as ML type/structure, printing verbatim. |
|
54 |
|
55 * Added antiquotation @{abbrev "c args"} which prints the abbreviation |
|
56 "c args == rhs" given in the current context. (Any number of |
|
57 arguments on the LHS may be given.) |
|
58 |
54 |
59 |
55 |
60 |
56 *** Pure *** |
61 *** Pure *** |
57 |
62 |
58 * class_package.ML offers a combination of axclasses and locales to |
63 * class_package.ML offers a combination of axclasses and locales to |