src/HOL/Metis.thy
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Mon, 21 May 2012 10:39:32 +0200 blanchet add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Fri, 24 Feb 2012 11:23:34 +0100 blanchet renamed 'try_methods' to 'try0'
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file
Tue, 15 Nov 2011 22:13:39 +0100 blanchet continued implementation of lambda-lifting in Metis
Fri, 02 Sep 2011 14:43:20 +0200 blanchet renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
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