equal
deleted
inserted
replaced
1 (* Title: Old_HOL/ex/ROOT.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Executes miscellaneous examples for Higher-Order Logic. |
|
7 *) |
|
8 |
|
9 HOL_build_completed; (*Cause examples to fail if HOL did*) |
|
10 |
|
11 writeln"Root file for HOL examples"; |
|
12 proof_timing := true; |
|
13 loadpath := ["ex"]; |
|
14 time_use "ex/cla.ML"; |
|
15 time_use "ex/meson.ML"; |
|
16 time_use "ex/mesontest.ML"; |
|
17 time_use_thy "String"; |
|
18 time_use_thy "InSort"; |
|
19 time_use_thy "Qsort"; |
|
20 time_use_thy "LexProd"; |
|
21 time_use_thy "Puzzle"; |
|
22 time_use_thy "NatSum"; |
|
23 time_use "ex/set.ML"; |
|
24 time_use_thy "SList"; |
|
25 time_use_thy "LList"; |
|
26 time_use_thy "Acc"; |
|
27 time_use_thy "PropLog"; |
|
28 time_use_thy "Term"; |
|
29 time_use_thy "Simult"; |
|
30 time_use_thy "MT"; |
|
31 |
|
32 make_chart (); (*make HTML chart*) |
|
33 |
|
34 writeln "END: Root file for HOL examples"; |
|