changeset 15647 | b1f486a9c56b |
parent 14694 | 49873d345a39 |
child 17644 | bd59bfd4bf37 |
15646:b45393fb38c0 | 15647:b1f486a9c56b |
---|---|
1 (* Title: HOL/Import/HOL/ROOT.ML |
1 (* Title: HOL/Import/HOL/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 with_path ".." use_thy "HOL4Compat"; |
|
7 with_path ".." use_thy "HOL4Syntax"; |
|
8 setmp quick_and_dirty true use_thy "HOL4Prob"; |
6 setmp quick_and_dirty true use_thy "HOL4Prob"; |
9 setmp quick_and_dirty true use_thy "HOL4"; |
7 setmp quick_and_dirty true use_thy "HOL4"; |