author | blanchet |
Tue, 28 Aug 2012 17:36:20 +0200 | |
changeset 48981 | 3517d6f50b12 |
parent 48738 | f8c1a5b9488f |
child 51397 | 03b586ee5930 |
permissions | -rw-r--r-- |
session LCF = Pure + description {* Author: Tobias Nipkow Copyright 1992 University of Cambridge *} options [document = false] theories LCF session "LCF-ex" in ex = LCF + description {* Author: Tobias Nipkow Copyright 1991 University of Cambridge Some examples from Lawrence Paulson's book Logic and Computation. *} options [document = false] theories Ex1 Ex2 Ex3 Ex4