author | wenzelm |
Tue, 24 Jul 2012 14:07:44 +0200 | |
changeset 48475 | 02dd825f5a4e |
child 48483 | 9bfb6978eb80 |
permissions | -rw-r--r-- |
session LCF! in "." = Pure + description {* Author: Tobias Nipkow Copyright 1992 University of Cambridge *} theories LCF session ex = LCF + description {* Author: Tobias Nipkow Copyright 1991 University of Cambridge Some examples from Lawrence Paulson's book Logic and Computation. *} theories Ex1 Ex2 Ex3 Ex4