src/HOL/Metis_Examples/Clausification.thy
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
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