equal
deleted
inserted
replaced
|
1 (* Title: FOL/ex/ROOT |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Executes all examples for First-Order Logic. |
|
7 *) |
|
8 |
|
9 writeln"Root file for FOL examples"; |
|
10 |
|
11 FOL_build_completed; (*Cause examples to fail if FOL did*) |
|
12 |
|
13 proof_timing := true; |
|
14 |
|
15 time_use "ex/intro.ML"; |
|
16 time_use_thy "ex/nat"; |
|
17 time_use "ex/foundn.ML"; |
|
18 time_use_thy "ex/prolog"; |
|
19 |
|
20 writeln"\n** Intuitionistic examples **\n"; |
|
21 time_use "ex/int.ML"; |
|
22 |
|
23 val thy = IFOL.thy and tac = Int.fast_tac 1; |
|
24 time_use "ex/prop.ML"; |
|
25 time_use "ex/quant.ML"; |
|
26 |
|
27 writeln"\n** Classical examples **\n"; |
|
28 time_use "ex/cla.ML"; |
|
29 time_use_thy "ex/if"; |
|
30 |
|
31 val thy = FOL.thy and tac = Cla.fast_tac FOL_cs 1; |
|
32 time_use "ex/prop.ML"; |
|
33 time_use "ex/quant.ML"; |
|
34 |
|
35 writeln"\n** Simplification examples **\n"; |
|
36 time_use_thy "ex/nat2"; |
|
37 time_use_thy "ex/list"; |
|
38 |
|
39 maketest"END: Root file for FOL examples"; |