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;
wenzelm@51397
     1
chapter LCF
wenzelm@51397
     2
wenzelm@48738
     3
session LCF = Pure +
wenzelm@48475
     4
  description {*
wenzelm@48475
     5
    Author:     Tobias Nipkow
wenzelm@48475
     6
    Copyright   1992  University of Cambridge
wenzelm@51403
     7
wenzelm@51403
     8
    Logic for Computable Functions.
wenzelm@51403
     9
wenzelm@51403
    10
    Useful references on LCF: Lawrence C. Paulson,
wenzelm@51403
    11
    Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
wenzelm@48475
    12
  *}
wenzelm@66444
    13
  sessions
wenzelm@66444
    14
    FOL
wenzelm@58974
    15
  theories
wenzelm@58974
    16
    LCF
wenzelm@48475
    17
wenzelm@58974
    18
    (* Some examples from Lawrence Paulson's book Logic and Computation *)
wenzelm@58974
    19
    "ex/Ex1"
wenzelm@58974
    20
    "ex/Ex2"
wenzelm@58974
    21
    "ex/Ex3"
wenzelm@58974
    22
    "ex/Ex4"