src/HOL/Metis_Examples/BT.thy
Wed, 28 Apr 2010 12:49:52 +0200 blanchet insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
Tue, 27 Apr 2010 18:07:51 +0200 blanchet redid the proofs with the latest Sledgehammer;
Tue, 20 Oct 2009 19:52:04 +0200 wenzelm modernized session Metis_Examples;
less more (0) tip