| author | wenzelm |
| Tue, 20 Nov 2018 13:46:13 +0100 | |
| changeset 69319 | baccaf89ca0d |
| parent 69272 | 15e9ed5b28fb |
| child 70675 | efd995488228 |
| 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) " sessions FOL theories LCF (* Some examples from Lawrence Paulson's book Logic and Computation *) "ex/Ex1" "ex/Ex2" "ex/Ex3" "ex/Ex4"