src/HOL/Metis_Examples/Clausification.thy
2013-01-03 blanchet 2013-01-03 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
2013-01-03 blanchet 2013-01-03 get rid of two-year-old hack, now that the "metis" skolemizer no longer gets stuck in HO unification
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2011-06-07 blanchet 2011-06-07 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
2011-06-06 blanchet 2011-06-06 tuned Metis examples