| changeset 33519 | e31a85f92ce9 |
| parent 30266 | 970bf4f594c9 |
| child 33700 | 768d14a67256 |
| 33518:24563731b9b2 | 33519:e31a85f92ce9 |
|---|---|
13 structure ML_Thms: ML_THMS = |
13 structure ML_Thms: ML_THMS = |
14 struct |
14 struct |
15 |
15 |
16 (* auxiliary facts table *) |
16 (* auxiliary facts table *) |
17 |
17 |
18 structure AuxFacts = ProofDataFun |
18 structure AuxFacts = Proof_Data |
19 ( |
19 ( |
20 type T = thm list Inttab.table; |
20 type T = thm list Inttab.table; |
21 fun init _ = Inttab.empty; |
21 fun init _ = Inttab.empty; |
22 ); |
22 ); |
23 |
23 |