17480

1 
(* Title: FOLP/ex/ROOT.ML

0

2 
ID: $Id$

1459

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1992 University of Cambridge


5 

17480

6 
Examples for FirstOrder Logic.

0

7 
*)


8 

1351

9 
time_use "intro.ML";


10 
time_use_thy "Nat";


11 
time_use "foundn.ML";

0

12 


13 
writeln"\n** Intuitionistic examples **\n";

1351

14 
time_use "int.ML";

0

15 

17480

16 
val thy = theory "IFOLP" and tac = IntPr.fast_tac 1;

1351

17 
time_use "prop.ML";


18 
time_use "quant.ML";

0

19 


20 
writeln"\n** Classical examples **\n";

1351

21 
time_use "cla.ML";


22 
time_use_thy "If";

0

23 

17480

24 
val thy = theory "FOLP" and tac = Cla.fast_tac FOLP_cs 1;

1351

25 
time_use "prop.ML";


26 
time_use "quant.ML";
