src/HOL/Metis_Examples/Abstraction.thy
Mon, 30 Jan 2012 17:15:59 +0100 blanchet example tuning
Mon, 02 Jan 2012 15:08:40 +0100 blanchet ported a dozen of proofs to the "set" type constructor
Sat, 24 Dec 2011 15:53:11 +0100 haftmann commented out examples which choke on strict set/pred distinction
Fri, 18 Nov 2011 11:47:12 +0100 blanchet more "metis" calls in example
Fri, 18 Nov 2011 11:47:12 +0100 blanchet example cleanup
Fri, 18 Nov 2011 11:47:12 +0100 blanchet example cleanup
Tue, 15 Nov 2011 12:39:49 +0100 huffman remove old-style semicolons
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuned Metis examples
Thu, 12 May 2011 15:29:19 +0200 blanchet remove problematic Isar proof
Thu, 24 Mar 2011 17:49:27 +0100 blanchet Metis examples use the new Skolemizer to test it
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Wed, 15 Dec 2010 11:26:28 +0100 blanchet example tuning
Wed, 01 Sep 2010 00:07:31 +0200 blanchet rename sledgehammer config attributes
Fri, 30 Apr 2010 14:00:09 +0200 blanchet minor improvements
Thu, 29 Apr 2010 19:02:04 +0200 blanchet redid some Sledgehammer/Metis proofs
Tue, 20 Oct 2009 19:52:04 +0200 wenzelm modernized session Metis_Examples;
less more (0) tip