src/FOL/ex/ROOT.ML
author wenzelm
Mon May 22 12:05:12 2000 +0200 (2000-05-22)
changeset 8909 96503b90307b
parent 6349 f7750d816c21
child 9000 c20d58286a51
permissions -rw-r--r--
added NatClass;
clasohm@1459
     1
(*  Title:      FOL/ex/ROOT
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Executes all examples for First-Order Logic. 
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
writeln"Root file for FOL examples";
clasohm@0
    10
wenzelm@4446
    11
set proof_timing;
clasohm@0
    12
clasohm@1351
    13
time_use     "intro.ML";
clasohm@1351
    14
time_use_thy "Nat";
clasohm@1351
    15
time_use     "foundn.ML";
clasohm@1351
    16
time_use_thy "Prolog";
clasohm@0
    17
clasohm@0
    18
writeln"\n** Intuitionistic examples **\n";
clasohm@1351
    19
time_use     "int.ML";
clasohm@0
    20
paulson@2601
    21
val thy = IFOL.thy  and  tac = IntPr.fast_tac 1;
clasohm@1351
    22
time_use     "prop.ML";
clasohm@1351
    23
time_use     "quant.ML";
clasohm@0
    24
clasohm@0
    25
writeln"\n** Classical examples **\n";
clasohm@1351
    26
time_use     "mini.ML";
clasohm@1351
    27
time_use     "cla.ML";
clasohm@1351
    28
time_use_thy "If";
clasohm@0
    29
clasohm@0
    30
val thy = FOL.thy  and  tac = Cla.fast_tac FOL_cs 1;
clasohm@1351
    31
time_use     "prop.ML";
clasohm@1351
    32
time_use     "quant.ML";
clasohm@0
    33
wenzelm@8909
    34
time_use_thy "NatClass";
wenzelm@8909
    35
clasohm@0
    36
writeln"\n** Simplification examples **\n";
clasohm@1351
    37
time_use_thy "Nat2";
clasohm@1351
    38
time_use_thy "List";
clasohm@0
    39
paulson@1549
    40
writeln"\n** How to declare an oracle **\n";
paulson@1549
    41
time_use_thy "IffOracle";