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