equal
deleted
inserted
replaced
9 * Command 'find_theorems': support "*" wildcard in "name:" criterion. |
9 * Command 'find_theorems': support "*" wildcard in "name:" criterion. |
10 |
10 |
11 |
11 |
12 *** Document preparation *** |
12 *** Document preparation *** |
13 |
13 |
14 * Added antiquotations @{ML_type text} and @{ML_struct} which check |
14 * Added antiquotations @{ML_type text} and @{ML_struct text} which |
15 the given source text as ML type/structure, printing verbatim. |
15 check the given source text as ML type/structure, printing verbatim. |
16 |
16 |
17 |
17 |
18 *** Pure *** |
18 *** Pure *** |
19 |
19 |
20 * Isar: improper proof element 'guess' is like 'obtain', but derives |
20 * Isar: improper proof element 'guess' is like 'obtain', but derives |