author  haftmann 
Tue, 10 Jul 2007 17:30:50 +0200  
changeset 23709  fd31da8f752a 
parent 23156  6ec9e29143e9 
child 23914  3e0424305fa4 
permissions  rwrr 
11675  1 
(* Title: FOL/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 

11675  6 
Examples for FirstOrder Logic. 
0  7 
*) 
8 

12369  9 
time_use_thy "First_Order_Logic"; 
12393  10 
time_use_thy "Natural_Numbers"; 
19819  11 
time_use_thy "Intro"; 
1351  12 
time_use_thy "Nat"; 
19819  13 
time_use_thy "Foundation"; 
1351  14 
time_use_thy "Prolog"; 
0  15 

14236  16 
time_use_thy "Intuitionistic"; 
0  17 

23156  18 
val thy = theory "IFOL" and tac = IntPr.fast_tac 1; 
1351  19 
time_use "prop.ML"; 
20 
time_use "quant.ML"; 

0  21 

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

19820  23 
time_use_thy "Miniscope"; 
14236  24 
time_use_thy "Classical"; 
1351  25 
time_use_thy "If"; 
0  26 

23156  27 
val thy = theory "FOL" and tac = Cla.fast_tac FOL_cs 1; 
1351  28 
time_use "prop.ML"; 
29 
time_use "quant.ML"; 

0  30 

8909  31 
time_use_thy "NatClass"; 
32 

1549  33 
time_use_thy "IffOracle"; 
17277
ab45d65bf204
make LocalesTest last, because it sets funny flags;
wenzelm
parents:
16168
diff
changeset

34 

ab45d65bf204
make LocalesTest last, because it sets funny flags;
wenzelm
parents:
16168
diff
changeset

35 
(*regression test for locales  sets several global flags!*) 
ab45d65bf204
make LocalesTest last, because it sets funny flags;
wenzelm
parents:
16168
diff
changeset

36 
time_use_thy "LocaleTest"; 