changeset 17644 | bd59bfd4bf37 |
parent 15647 | b1f486a9c56b |
child 17648 | 7568d2cc560e |
17643:7e417a7cbf9f | 17644:bd59bfd4bf37 |
---|---|
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 setmp quick_and_dirty true use_thy "HOL4Prob"; |
6 set show_types; set show_sorts; |
7 setmp quick_and_dirty true use_thy "HOL4"; |
7 use_thy "HOL4Prob"; |
8 use_thy "HOL4"; |