changeset 6252 | 935f183bf406 |
child 6349 | f7750d816c21 |
6251:4d89d4f0ab17 | 6252:935f183bf406 |
---|---|
1 (* Title: LK/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 Classical Logic. |
|
7 *) |
|
8 |
|
9 Sequents_build_completed; (*Cause examples to fail if Sequents did*) |
|
10 |
|
11 writeln"Root file for LK examples"; |
|
12 |
|
13 set proof_timing; |
|
14 time_use "prop.ML"; |
|
15 time_use "quant.ML"; |
|
16 time_use "hardquant.ML"; |