src/HOL/Metis_Examples/Tarski.thy
2015-10-10 wenzelm 2015-10-10 prefer symbols;
2014-11-08 wenzelm 2014-11-08 updated some sledgehammer proofs -- much faster;
2014-11-08 wenzelm 2014-11-08 updated sledgehammer proof after breakdown of metis (exception Type.TUNIFY);
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2013-01-03 blanchet 2013-01-03 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
2012-03-20 blanchet 2012-03-20 tune Metis example
2012-03-01 haftmann 2012-03-01 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-12-01 blanchet 2011-12-01 tuning
2011-06-06 blanchet 2011-06-06 tuned Metis examples
2011-05-12 blanchet 2011-05-12 prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior
2011-03-24 blanchet 2011-03-24 Metis examples use the new Skolemizer to test it
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-15 blanchet 2010-12-15 example tuning
2010-12-15 blanchet 2010-12-15 added example to exercise higher-order reasoning with Sledgehammer and Metis
2010-09-01 blanchet 2010-09-01 rename sledgehammer config attributes
2010-06-28 blanchet 2010-06-28 no setup is necessary anymore
2010-04-29 blanchet 2010-04-29 more neg_clausify proofs that get replaced by direct proofs
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-08 wenzelm 2010-02-08 modernized some syntax translations;
2009-10-20 wenzelm 2009-10-20 modernized session Metis_Examples;