2013-05-07 traytel 2013-05-07 got rid of the set based relator---use (binary) predicate based relator instead
2013-04-24 blanchet 2013-04-24 renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-10-16 wenzelm 2012-10-16 clarified defer/prefer: more specific errors;
2012-09-30 traytel 2012-09-30 got rid of subst_tac alias
2012-09-28 traytel 2012-09-28 tuned tactics
2012-09-27 traytel 2012-09-27 tuned tactic; got rid of substs_tac alias
2012-09-26 blanchet 2012-09-26 parameterized "subst_tac"
2012-09-21 blanchet 2012-09-21 renamed LFP low-level rel property to have ctor not dtor in its name
2012-09-21 blanchet 2012-09-21 renamed "rel_simp" to "dtor_rel" and similarly for "srel"
2012-09-21 blanchet 2012-09-21 renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"