author | paulson |
Tue, 29 Aug 2017 17:41:27 +0100 | |
changeset 66553 | 6ab32ffb2bdd |
parent 66444 | 6d2d993fa76e |
child 66946 | 3d8fd98c7c86 |
permissions | -rw-r--r-- |
chapter LCF session LCF = Pure + description {* Author: Tobias Nipkow Copyright 1992 University of Cambridge Logic for Computable Functions. Useful references on LCF: Lawrence C. Paulson, Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987) *} options [document = false] sessions FOL theories LCF (* Some examples from Lawrence Paulson's book Logic and Computation *) "ex/Ex1" "ex/Ex2" "ex/Ex3" "ex/Ex4"