author  paulson 
Tue, 27 Jul 1999 18:50:14 +0200  
changeset 7091  b76a26835a5c 
parent 6349  f7750d816c21 
child 9000  c20d58286a51 
permissions  rwrr 
6252  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 
writeln"Root file for LK examples"; 

10 

11 
set proof_timing; 

12 
time_use "prop.ML"; 

13 
time_use "quant.ML"; 

14 
time_use "hardquant.ML"; 

7091
b76a26835a5c
Sequents/LK/Nat: new example of simplification in LK
paulson
parents:
6349
diff
changeset

15 
use_thy "Nat"; 