2016-07-20 wenzelm 2016-07-20 moved method "use" to Pure; more documentation;
2016-06-07 wenzelm 2016-06-07 less ambitious arguments: thms only, no context declaration;
2016-06-07 wenzelm 2016-06-07 added method operator "use";
2016-01-12 matichuk 2016-01-12 remove Eisbach's dependency on HOL
2015-12-23 wenzelm 2015-12-23 tuned module arrangement;
2015-12-16 wenzelm 2015-12-16 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-07-01 wenzelm 2015-07-01 support for subgoal focus command;
2015-05-16 wenzelm 2015-05-16 updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
2015-05-03 wenzelm 2015-05-03 updated Eisbach, using version fb741500f533 of its Bitbucket repository;
2015-04-30 wenzelm 2015-04-30 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
2015-04-17 wenzelm 2015-04-17 added Eisbach, using version 3752768caa17 of its Bitbucket repository;