isabelle: src/HOL/Metis_Examples/ROOT.ML@d012947edd36 (annotated)

33027 9cf389429f6d modernized session Metis_Examples; wenzelm parents: 25709 diff changeset	1	(* Title: HOL/Metis_Examples/ROOT.ML
23449 dd874e6a3282 integration of Metis prover paulson parents: diff changeset	2	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: 33027 diff changeset	3	Author: Jasmin Blanchette, TU Muenchen
23449 dd874e6a3282 integration of Metis prover paulson parents: diff changeset	4
41141 ad923cdd4a5d added example to exercise higher-order reasoning with Sledgehammer and Metis blanchet parents: 33027 diff changeset	5	Testing Metis and Sledgehammer.
23449 dd874e6a3282 integration of Metis prover paulson parents: diff changeset	6	*)
dd874e6a3282 integration of Metis prover paulson parents: diff changeset	7
42343 118cc349de35 compile blanchet parents: 42338 diff changeset	8	use_thys ["Abstraction", "BigO", "BT", "Clausify", "HO_Reas", "Message",
42338 802f2fe7a0c9 started clausifier examples blanchet parents: 41144 diff changeset	9	"Tarski", "TransClosure", "set"];