changeset 81933 | cb05f8d3fd05 |
parent 81905 | 5fd1dea4eb61 |
81932:0a1ed07a458a | 81933:cb05f8d3fd05 |
---|---|
1 (* Title: HOL/Import/import_data.ML |
1 (* Title: HOL/Import/import_data.ML |
2 Author: Cezary Kaliszyk, University of Innsbruck |
2 Author: Cezary Kaliszyk, University of Innsbruck |
3 Author: Alexander Krauss, QAware GmbH |
3 Author: Alexander Krauss, QAware GmbH |
4 Author: Makarius |
|
4 |
5 |
5 Importer data. |
6 Importer data. |
6 *) |
7 *) |
7 |
8 |
8 signature IMPORT_DATA = |
9 signature IMPORT_DATA = |