author | wenzelm |
Sat, 27 Feb 2021 21:36:58 +0100 (2021-02-27) | |
changeset 73323 | c2ab1a970e82 |
parent 70678 | 36c8c32346cb |
child 75992 | 1f6d79b62222 |
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 directories "ex" theories LCF (* Some examples from Lawrence Paulson's book Logic and Computation *) "ex/Ex1" "ex/Ex2" "ex/Ex3" "ex/Ex4"