isabelle: src/HOL/MetisExamples/ROOT.ML@f8712e98756a (annotated)

23449 dd874e6a3282 integration of Metis prover paulson parents: diff changeset	1	(* Title: HOL/MetisExamples/ROOT.ML
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	2	ID: $Id$
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	4
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	5	Testing the metis method
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	6	*)
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	7
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	8	time_use_thy "set";
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	9	time_use_thy "BigO";
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	10	time_use_thy "Abstraction";
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	11	time_use_thy "BT";
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	12	time_use_thy "Message";
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	13	time_use_thy "Tarski";
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	14	time_use_thy "TransClosure";