src/HOL/Metis_Examples/HO_Reas.thy
Sun, 01 May 2011 18:37:24 +0200 blanchet more higher-order tests for Sledgehammer/ATP
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 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
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
less more (0) tip