(* Title: HOL/Metis_Examples/ROOT.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Testing Metis and Sledgehammer. *) use_thys ["Abstraction", "BigO", "BT", "Clausify", "HO_Reas", "Message", "Tarski", "TransClosure", "set"];