| changeset 163 | 2319cff107f0 |
| parent 124 | 0b9fa606a746 |
| child 164 | 3f617d7a2691 |
| 162:3fb9f820a294 | 163:2319cff107f0 |
|---|---|
1 theory Ind_Code |
1 theory Ind_Code |
2 imports "../Base" Simple_Inductive_Package |
2 imports "../Base" Simple_Inductive_Package |
3 begin |
3 begin |
4 |
|
5 text {* |
|
6 What does the @{ML Thm.internalK} do, in the LocalTheory.define Thm.internalK? |
|
7 *} |
|
8 |
|
4 |
9 |
5 text {* |
10 text {* |
6 |
11 |
7 @{ML_chunk [display,gray] definitions_aux} |
12 @{ML_chunk [display,gray] definitions_aux} |
8 @{ML_chunk [display,gray,linenos] definitions} |
13 @{ML_chunk [display,gray,linenos] definitions} |