(* Title: LCF/ROOT.ML Author: Tobias Nipkow Copyright 1992 University of Cambridge *) use_thys ["LCF"];