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