src/HOL/Eisbach/method_closure.ML
2016-07-20 wenzelm 2016-07-20 moved method "use" to Pure; more documentation;
2016-06-07 wenzelm 2016-06-07 clarified signature;
2016-05-31 matichuk 2016-05-31 allow multiple recursive methods to co-exist in order to support mutual recursion;
2016-05-30 matichuk 2016-05-30 apply current morphism to method text before evaluating;
2016-04-01 wenzelm 2016-04-01 removed redundant Position.set_range -- already done in Position.range;
2016-01-12 matichuk 2016-01-12 remove unused code
2016-01-09 wenzelm 2016-01-09 suppress somewhat pointless description (NB: this is displayed in 'print_methods');
2016-01-06 wenzelm 2016-01-06 more systematic treatment of dynamic facts, when forming closure;
2016-01-06 wenzelm 2016-01-06 proper Pattern.match and corresponding Envir.subst_term, instead of Envir.norm_term of unify-family;
2016-01-05 wenzelm 2016-01-05 tuned;
2016-01-05 wenzelm 2016-01-05 tuned;
2016-01-05 wenzelm 2016-01-05 more realistic Eisbach method invocation from ML; misc tuning and clarification;
2016-01-05 wenzelm 2016-01-05 unused;
2015-12-23 wenzelm 2015-12-23 tuned;
2015-12-23 wenzelm 2015-12-23 tuned module arrangement;
2015-12-23 wenzelm 2015-12-23 tuned module arrangement;
2015-12-23 wenzelm 2015-12-23 check and report source at most once, notably in body of "match" method;
2015-12-22 wenzelm 2015-12-22 more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
2015-12-22 wenzelm 2015-12-22 proper full name within the name space of the method definition;
2015-12-22 wenzelm 2015-12-22 tuned signature; tuned;
2015-12-22 wenzelm 2015-12-22 tuned -- with subtle change of order of evaluation;
2015-12-22 wenzelm 2015-12-22 more accurate lookup of dynamic facts;
2015-12-22 wenzelm 2015-12-22 tuned;
2015-12-22 wenzelm 2015-12-22 tuned;
2015-12-22 wenzelm 2015-12-22 tuned signature;
2015-12-22 wenzelm 2015-12-22 tuned;
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-12-15 wenzelm 2015-12-15 unused;
2015-12-09 wenzelm 2015-12-09 tuned signature;
2015-12-09 wenzelm 2015-12-09 tuned signature;
2015-12-09 wenzelm 2015-12-09 more direct use of Token.src as token list; tuned signature; tuned;
2015-12-09 wenzelm 2015-12-09 unused;
2015-12-09 wenzelm 2015-12-09 clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;
2015-06-22 wenzelm 2015-06-22 tuned signature;
2015-06-22 wenzelm 2015-06-22 tuned whitespace;
2015-06-14 wenzelm 2015-06-14 tuned signature;
2015-06-09 wenzelm 2015-06-09 tuned signature;
2015-06-07 wenzelm 2015-06-07 tuned signature;
2015-05-17 wenzelm 2015-05-17 updated Eisbach, using version 134bc592909c of its Bitbucket repository;
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;