author | wenzelm |
Tue, 24 Nov 1998 12:03:09 +0100 | |
changeset 5953 | d6017ce6b93e |
parent 4905 | be73ddff6c5a |
child 6349 | f7750d816c21 |
permissions | -rw-r--r-- |
(* Title: LCF/ex/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1991 University of Cambridge Some examples from Lawrence Paulson's book Logic and Computation. *) writeln"Root file for LCF examples"; LCF_build_completed; (*Cause examples to fail if LCF did*) set proof_timing; use_thy "Ex1"; use_thy "Ex2"; use_thy "Ex3"; use_thy "Ex4";