| changeset 15836 | b805d85909c7 |
| parent 15801 | d2f5ca3c048d |
| child 17170 | cbe14eb12729 |
| 15835:fdf678bec567 | 15836:b805d85909c7 |
|---|---|
1 (* Title: Pure/Thy/thm_database.ML |
1 (* Title: Pure/Thy/thm_database.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
4 |
5 Interface to the theorem database. |
5 Theorem database ML interface. |
6 *) |
6 *) |
7 |
7 |
8 signature BASIC_THM_DATABASE = |
8 signature BASIC_THM_DATABASE = |
9 sig |
9 sig |
10 val store_thm: string * thm -> thm |
10 val store_thm: string * thm -> thm |