equal
deleted
inserted
replaced
10 "Intro", |
10 "Intro", |
11 "Nat", |
11 "Nat", |
12 "Foundation", |
12 "Foundation", |
13 "If", |
13 "If", |
14 "Intuitionistic", |
14 "Intuitionistic", |
15 "Classical" |
15 "Classical", |
|
16 "Propositional_Int", |
|
17 "Quantifiers_Int", |
|
18 "Propositional_Cla", |
|
19 "Quantifiers_Cla" |
16 ]; |
20 ]; |
17 |
|
18 val thy = theory "IFOLP" and tac = IntPr.fast_tac 1; |
|
19 time_use "prop.ML"; |
|
20 time_use "quant.ML"; |
|
21 |
|
22 val thy = theory "FOLP" and tac = Cla.fast_tac FOLP_cs 1; |
|
23 time_use "prop.ML"; |
|
24 time_use "quant.ML"; |
|