equal
deleted
inserted
replaced
1 (* Title: HOL/ex/ROOT.ML |
1 (* Title: HOL/ex/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 |
3 |
4 Miscellaneous examples for Higher-Order Logic. |
4 Miscellaneous examples for Higher-Order Logic. |
5 *) |
5 *) |
|
6 |
|
7 no_document time_use_thy "Classpackage"; |
|
8 no_document time_use_thy "Codegenerator"; |
6 |
9 |
7 time_use_thy "Higher_Order_Logic"; |
10 time_use_thy "Higher_Order_Logic"; |
8 time_use_thy "Abstract_NAT"; |
11 time_use_thy "Abstract_NAT"; |
9 |
12 |
10 time_use_thy "Recdefs"; |
13 time_use_thy "Recdefs"; |
55 else |
58 else |
56 (); |
59 (); |
57 |
60 |
58 time_use_thy "Refute_Examples"; |
61 time_use_thy "Refute_Examples"; |
59 time_use_thy "Quickcheck_Examples"; |
62 time_use_thy "Quickcheck_Examples"; |
60 no_document time_use_thy "Classpackage"; |
|
61 no_document time_use_thy "Codegenerator"; |
|
62 no_document time_use_thy "nbe"; |
63 no_document time_use_thy "nbe"; |
63 |
64 |
64 no_document use_thy "Word"; |
65 no_document use_thy "Word"; |
65 time_use_thy "Adder"; |
66 time_use_thy "Adder"; |
66 |
67 |