src/HOL/Metis.thy
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
Fri, 27 May 2011 10:30:08 +0200 blanchet renamed "try" "try_methods"
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Thu, 14 Apr 2011 11:24:05 +0200 blanchet make 48170228f562 work also with "HO_Reas" examples
Wed, 15 Dec 2010 11:26:28 +0100 blanchet added Sledgehammer support for higher-order propositional reasoning
Tue, 07 Dec 2010 09:58:56 +0100 blanchet load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
Mon, 11 Oct 2010 18:03:47 +0700 blanchet "setup" in theory
Tue, 05 Oct 2010 12:04:49 +0200 blanchet hide one more name
Tue, 05 Oct 2010 11:45:10 +0200 blanchet hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
Mon, 04 Oct 2010 22:51:53 +0200 blanchet tuning
Mon, 04 Oct 2010 22:45:09 +0200 blanchet move Metis into Plain
Wed, 20 Jun 2007 22:07:52 +0200 wenzelm The Metis prover (slightly modified version from Larry);
less more (0) tip