src/HOL/Metis_Examples/Tarski.thy
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;