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 

25991

9 
use_thys [


10 
"Intro",


11 
"Nat",


12 
"Foundation",


13 
"If"


14 
];

0

15 


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

1351

17 
time_use "int.ML";

0

18 

17480

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

1351

20 
time_use "prop.ML";


21 
time_use "quant.ML";

0

22 


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

1351

24 
time_use "cla.ML";

0

25 

17480

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

1351

27 
time_use "prop.ML";


28 
time_use "quant.ML";
