| changeset 118 | 5f003fdf2653 |
| parent 114 | 13fd0a83d3c3 |
| child 120 | c39f83d8daeb |
| 117:796c6ea633b3 | 118:5f003fdf2653 |
|---|---|
521 @{ML_file "Pure/thm.ML"}. |
521 @{ML_file "Pure/thm.ML"}. |
522 \end{readmore} |
522 \end{readmore} |
523 |
523 |
524 *} |
524 *} |
525 |
525 |
526 section {* Theories and Local Theories *} |
|
527 |
|
526 section {* Storing Theorems *} |
528 section {* Storing Theorems *} |
527 |
529 |
528 text {* @{ML PureThy.add_thms_dynamic} *} |
530 text {* @{ML PureThy.add_thms_dynamic} *} |
529 |
531 |
530 section {* Theorem Attributes *} |
532 section {* Theorem Attributes *} |