equal
deleted
inserted
replaced
1 |
1 |
2 theory NamedThms |
2 theory NamedThms |
3 imports Main |
3 imports Main |
|
4 uses "antiquote_setup.ML" |
|
5 "antiquote_setup_plus.ML" |
4 begin |
6 begin |
5 |
|
6 |
7 |
7 section {* Accumulate a List of Theorems under a Name *} |
8 section {* Accumulate a List of Theorems under a Name *} |
8 |
9 |
9 |
10 |
10 text {* |
11 text {* |
51 \begin{readmore} |
52 \begin{readmore} |
52 For more information see @{ML_file "Pure/Tools/named_thms.ML"}. |
53 For more information see @{ML_file "Pure/Tools/named_thms.ML"}. |
53 \end{readmore} |
54 \end{readmore} |
54 *} |
55 *} |
55 |
56 |
|
57 text {* |
|
58 (FIXME: maybe add a comment about the case when the theorems |
|
59 to be added need to satisfy certain properties) |
|
60 |
|
61 *} |
|
62 |
56 |
63 |
57 end |
64 end |
58 |
65 |
59 |
66 |
60 |
67 |