changeset 23449 | dd874e6a3282 |
child 25709 | 43a1f08c5a29 |
23448:020381339d87 | 23449:dd874e6a3282 |
---|---|
1 (* Title: HOL/MetisExamples/ROOT.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
|
5 Testing the metis method |
|
6 *) |
|
7 |
|
8 time_use_thy "set"; |
|
9 time_use_thy "BigO"; |
|
10 time_use_thy "Abstraction"; |
|
11 time_use_thy "BT"; |
|
12 time_use_thy "Message"; |
|
13 time_use_thy "Tarski"; |
|
14 time_use_thy "TransClosure"; |