(* Title: HOL/MetisExamples/ROOT.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Testing the metis method. *) use_thys ["set", "BigO", "Abstraction", "BT", "Message", "Tarski", "TransClosure"];