src/HOL/Metis_Examples/Message.thy
Wed, 15 Dec 2010 11:26:28 +0100 blanchet added example to exercise higher-order reasoning with Sledgehammer and Metis
less more (0) -1 tip