changeset 25374 | 7657a081fcb4 |
parent 17624 | da9a5efecde7 |
child 37296 | 1fad5b94c0ae |
25373:ccbf65080fdf | 25374:7657a081fcb4 |
---|---|
1 (* Title: HOL/Import/ROOT.ML |
1 (* Title: HOL/Import/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Sebastian Skalberg (TU Muenchen) |
3 Author: Sebastian Skalberg (TU Muenchen) |
4 *) |
4 *) |
5 |
5 |
6 proofs := 0; |
6 Proofterm.proofs := 0; |
7 use_thy "HOL4Compat"; |
7 use_thy "HOL4Compat"; |
8 use_thy "HOL4Syntax"; |
8 use_thy "HOL4Syntax"; |