src/HOL/Metis_Examples/Clausification.thy
Thu, 03 Jan 2013 13:28:37 +0100 blanchet get rid of two-year-old hack, now that the "metis" skolemizer no longer gets stuck in HO unification
Tue, 03 Apr 2012 16:26:48 +0200 kuncar new package Lifting - initial commit
Tue, 07 Jun 2011 08:52:35 +0200 blanchet obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
Mon, 06 Jun 2011 20:36:35 +0200 blanchet tuned Metis examples
less more (0) tip