src/HOL/Metis_Examples/Message.thy
Mon, 02 Jan 2012 14:45:13 +0100 blanchet reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow
Sat, 24 Dec 2011 15:53:10 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set`
Sun, 20 Nov 2011 21:05:23 +0100 wenzelm eliminated obsolete "standard";
Tue, 15 Nov 2011 12:51:14 +0100 huffman remove one more old-style semicolon
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
Sat, 23 Apr 2011 13:00:19 +0200 wenzelm modernized specifications;
Thu, 24 Mar 2011 17:49:27 +0100 blanchet Metis examples use the new Skolemizer to test it
Wed, 15 Dec 2010 11:26:28 +0100 blanchet example tuning
Wed, 15 Dec 2010 11:26:28 +0100 blanchet added example to exercise higher-order reasoning with Sledgehammer and Metis
Thu, 09 Sep 2010 12:28:00 +0200 blanchet "resurrected" a Metis proof
Fri, 14 May 2010 11:24:49 +0200 blanchet improved Sledgehammer proofs
Fri, 30 Apr 2010 18:29:04 +0200 wenzelm eliminated spurious sledgehammer invocation;
Wed, 28 Apr 2010 22:36:39 +0200 blanchet redo some of the metis proofs
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Thu, 11 Feb 2010 21:33:25 +0100 wenzelm modernized syntax/translations;
Wed, 10 Feb 2010 15:14:01 +0100 haftmann minor metis proof tuning
Mon, 08 Feb 2010 21:28:27 +0100 wenzelm modernized some syntax translations;
Tue, 20 Oct 2009 19:52:04 +0200 wenzelm modernized session Metis_Examples;
less more (0) tip