make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
(* Title: CTT/ROOT.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
use_thys ["Main"];