src/HOL/Eisbach/eisbach_rule_insts.ML
2016-01-13 wenzelm 2016-01-13 Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
2016-01-12 matichuk 2016-01-12 remove unused code
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-12-15 wenzelm 2015-12-15 tuned signature -- clarified modules;
2015-08-12 Daniel Matichuk 2015-08-12 clarify type vs. term instantiation when forming closure;
2015-07-26 wenzelm 2015-07-26 updated to infer_instantiate;
2015-07-05 wenzelm 2015-07-05 clarified context;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-06-22 wenzelm 2015-06-22 tuned whitespace;
2015-06-15 wenzelm 2015-06-15 redundant: read = check o parse;
2015-06-14 wenzelm 2015-06-14 tuned signature;
2015-06-07 wenzelm 2015-06-07 tuned signature;
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-17 wenzelm 2015-04-17 added Eisbach, using version 3752768caa17 of its Bitbucket repository;