inhabitance goal is now stated in original form and result contracted --
the previous attempt with contracted goal and initial unfolding did not work,
because it disrupted the Isar proof structure (e.g. ?thesis);
(* Title: HOL/MetisExamples/ROOT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Testing the metis method.
*)
use_thys ["set", "BigO", "Abstraction", "BT", "Message", "Tarski", "TransClosure"];