equal
deleted
inserted
replaced
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 Examples for First-Order Logic. |
6 Examples for First-Order Logic. |
7 *) |
7 *) |
8 |
8 |
9 time_use_thy "First_Order_Logic"; |
9 use_thys [ |
10 time_use_thy "Natural_Numbers"; |
10 "First_Order_Logic", |
11 time_use_thy "Intro"; |
11 "Natural_Numbers", |
12 time_use_thy "Nat"; |
12 "Intro", |
13 time_use_thy "Foundation"; |
13 "Nat", |
14 time_use_thy "Prolog"; |
14 "Foundation", |
|
15 "Prolog", |
15 |
16 |
16 time_use_thy "Intuitionistic"; |
17 "Intuitionistic", |
|
18 "Propositional_Int", |
|
19 "Quantifiers_Int", |
17 |
20 |
18 val thy = theory "IFOL" and tac = IntPr.fast_tac 1; |
21 "Classical", |
19 time_use "prop.ML"; |
22 "Propositional_Cla", |
20 time_use "quant.ML"; |
23 "Quantifiers_Cla", |
|
24 "Miniscope", |
|
25 "If", |
21 |
26 |
22 writeln"\n** Classical examples **\n"; |
27 "NatClass", |
23 time_use_thy "Miniscope"; |
28 "IffOracle" |
24 time_use_thy "Classical"; |
29 ]; |
25 time_use_thy "If"; |
|
26 |
|
27 val thy = theory "FOL" and tac = Cla.fast_tac FOL_cs 1; |
|
28 time_use "prop.ML"; |
|
29 time_use "quant.ML"; |
|
30 |
|
31 time_use_thy "NatClass"; |
|
32 |
|
33 time_use_thy "IffOracle"; |
|
34 |
30 |
35 (*regression test for locales -- sets several global flags!*) |
31 (*regression test for locales -- sets several global flags!*) |
36 time_use_thy "LocaleTest"; |
32 no_document use_thy "LocaleTest"; |