src/HOL/Metis.thy
Fri, 18 Mar 2016 21:21:09 +0100 wenzelm clarified print depth;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Wed, 29 Oct 2014 14:05:36 +0100 wenzelm modernized setup;
Tue, 13 May 2014 11:10:23 +0200 blanchet hide more internal names
Tue, 25 Mar 2014 19:03:02 +0100 wenzelm proper configuration option "ML_print_depth";
Sun, 16 Feb 2014 13:56:48 +0100 haftmann eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)
Thu, 30 Jan 2014 13:38:28 +0100 blanchet added 'algebra' and 'meson' to 'try0'
Fri, 18 Oct 2013 10:43:21 +0200 blanchet killed more "no_atp"s
Sat, 13 Jul 2013 00:50:49 +0200 wenzelm hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
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