| changeset 119 | 4536782969fa |
| parent 74 | f6f8f8ba1eb1 |
| 118:5f003fdf2653 | 119:4536782969fa |
|---|---|
1 theory NamedThms |
1 theory NamedThms |
2 imports "../Base" |
2 imports "../Base" |
3 begin |
3 begin |
4 |
4 |
5 section {* Accumulate a List of Theorems under a Name *} |
5 section {* Accumulate a List of Theorems under a Name\label{rec:named} *} |
6 |
6 |
7 |
7 |
8 text {* |
8 text {* |
9 {\bf Problem:} |
9 {\bf Problem:} |
10 Your tool @{text foo} works with special rules, called @{text foo}-rules. |
10 Your tool @{text foo} works with special rules, called @{text foo}-rules. |