1chapter LCF
2
3session 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  directories "ex"
16  theories
17    LCF
18    (* Some examples from Lawrence Paulson's book Logic and Computation *)
19    "ex/Ex1"
20    "ex/Ex2"
21    "ex/Ex3"
22    "ex/Ex4"
23