changeset 4905 | be73ddff6c5a |
parent 4446 | 097004a470fb |
child 6349 | f7750d816c21 |
--- a/src/LCF/ex/ROOT.ML Fri May 08 10:15:39 1998 +0200 +++ b/src/LCF/ex/ROOT.ML Fri May 08 13:54:45 1998 +0200 @@ -1,7 +1,17 @@ +(* 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 "ex.ML"; +use_thy "Ex1"; +use_thy "Ex2"; +use_thy "Ex3"; +use_thy "Ex4";