changeset 17624 | da9a5efecde7 |
parent 14684 | d796124e435c |
child 25374 | 7657a081fcb4 |
17623:ae4af66b3072 | 17624:da9a5efecde7 |
---|---|
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 use_thy "HOL4Compat"; |
7 use_thy "HOL4Compat"; |
7 use_thy "HOL4Syntax"; |
8 use_thy "HOL4Syntax"; |