adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies
(* 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"];