author  wenzelm 
Sun, 26 Nov 2006 23:43:53 +0100  
changeset 21539  c5cf9243ad62 
parent 19820  0d7564c798d0 
child 22822  c1a6a2159e69 
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 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2236
diff
changeset

18 
val thy = IFOL.thy 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 

27 
val thy = FOL.thy 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 

0  33 
writeln"\n** Simplification examples **\n"; 
1351  34 
time_use_thy "Nat2"; 
35 
time_use_thy "List"; 

0  36 

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

38 

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

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

40 
time_use_thy "LocaleTest"; 