src/LCF/ROOT
author wenzelm
Mon Oct 30 20:04:10 2017 +0100 (19 months ago)
changeset 66946 3d8fd98c7c86
parent 66444 6d2d993fa76e
child 69272 15e9ed5b28fb
permissions -rw-r--r--
ROOT cleanup: empty 'document_files' means there is no document;
     1 chapter LCF
     2 
     3 session LCF = Pure +
     4   description {*
     5     Author:     Tobias Nipkow
     6     Copyright   1992  University of Cambridge
     7 
     8     Logic for Computable Functions.
     9 
    10     Useful references on LCF: Lawrence C. Paulson,
    11     Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
    12   *}
    13   sessions
    14     FOL
    15   theories
    16     LCF
    17 
    18     (* Some examples from Lawrence Paulson's book Logic and Computation *)
    19     "ex/Ex1"
    20     "ex/Ex2"
    21     "ex/Ex3"
    22     "ex/Ex4"