let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
(* 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", "HO_Reas", "Message", "Tarski",
"TransClosure", "set"];