src/LCF/ROOT
author wenzelm
Wed May 16 23:13:33 2018 +0200 (15 months ago)
changeset 68199 f551dd2178ab
parent 66946 3d8fd98c7c86
child 69272 15e9ed5b28fb
permissions -rw-r--r--
proper PIDE positions;
     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"