equal
deleted
inserted
replaced
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
4 |
5 Derived theory operations. |
5 Derived theory operations. |
6 |
6 |
7 TODO: |
7 TODO: |
8 - add_constdefs (atomic!); |
8 - pure_thy.ML: add_constdefs (atomic!); |
9 - load theory; |
|
10 - 'methods' section (proof macros, ML method defs) (!?); |
9 - 'methods' section (proof macros, ML method defs) (!?); |
11 - next_block: ProofHistory open / close (!?); |
10 - next_block: ProofHistory open / close (!?); |
12 *) |
11 *) |
13 |
12 |
14 signature ISAR_THY = |
13 signature ISAR_THY = |