src/LCF/ROOT.ML
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 9000 c20d58286a51
child 17247 6927a62c77dc
permissions -rw-r--r--
added HOL/Prolog
     1 (*  Title:      LCF/ROOT.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1992  University of Cambridge
     5 
     6 LCF on top of First-Order Logic.
     7 
     8 This theory is based on Lawrence Paulson's book Logic and Computation.
     9 *)
    10 
    11 val banner = "Logic for Computable Functions (in FOL)";
    12 writeln banner;
    13 
    14 print_depth 1;
    15 use_thy "LCF";
    16 use"simpdata.ML";
    17 use_thy"pair";
    18 use_thy"fix";