put MiniSat back first -- Torlak's eval seemed to suggest that Crypto and Lingeling were better, but Crypto is slower on "Nitpick_Examples" and Crypto crashes
(* Title: HOL/Import/ROOT.ML
Author: Sebastian Skalberg (TU Muenchen)
*)
use_thys ["HOL4Compat", "HOL4Syntax"];