src/HOL/Metis_Examples/Abstraction.thy
2014-03-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2014-02-14 blanchet 2014-02-14 merged 'List.map' and 'List.list.map'
2012-01-30 blanchet 2012-01-30 example tuning
2012-01-02 blanchet 2012-01-02 ported a dozen of proofs to the "set" type constructor
2011-12-24 haftmann 2011-12-24 commented out examples which choke on strict set/pred distinction
2011-11-18 blanchet 2011-11-18 more "metis" calls in example
2011-11-18 blanchet 2011-11-18 example cleanup
2011-11-18 blanchet 2011-11-18 example cleanup
2011-11-15 huffman 2011-11-15 remove old-style semicolons
2011-06-06 blanchet 2011-06-06 tuned Metis examples
2011-05-12 blanchet 2011-05-12 remove problematic Isar proof
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-09-01 blanchet 2010-09-01 rename sledgehammer config attributes
2010-04-30 blanchet 2010-04-30 minor improvements
2010-04-29 blanchet 2010-04-29 redid some Sledgehammer/Metis proofs
2009-10-20 wenzelm 2009-10-20 modernized session Metis_Examples;