(* Title: LCF/ex/ROOT.ML Author: Tobias Nipkow Copyright 1991 University of Cambridge Some examples from Lawrence Paulson's book Logic and Computation. *) use_thys ["Ex1", "Ex2", "Ex3", "Ex4"];