src/HOL/Metis_Examples/ROOT.ML
author wenzelm
Mon, 25 Oct 2010 21:23:09 +0200
changeset 40133 b61d52de66f0
parent 33027 9cf389429f6d
child 41141 ad923cdd4a5d
permissions -rw-r--r--
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);

(*  Title:      HOL/Metis_Examples/ROOT.ML
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Testing the metis method.
*)

use_thys ["set", "BigO", "Abstraction", "BT", "Message", "Tarski", "TransClosure"];