src/LCF/ROOT.ML
changeset 9000 c20d58286a51
parent 6349 f7750d816c21
child 17247 6927a62c77dc
equal deleted inserted replaced
8999:ad8260dc6e4a 9000:c20d58286a51
     1 (*  Title:      LCF/ROOT
     1 (*  Title:      LCF/ROOT.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     3     Author:     Tobias Nipkow
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Adds LCF to a database containing First-Order Logic.
     6 LCF on top of First-Order Logic.
     7 
     7 
     8 This theory is based on Lawrence Paulson's book Logic and Computation.
     8 This theory is based on Lawrence Paulson's book Logic and Computation.
     9 *)
     9 *)
    10 
    10 
    11 val banner = "Logic for Computable Functions (in FOL)";
    11 val banner = "Logic for Computable Functions (in FOL)";