src/HOL/Eisbach/match_method.ML
2016-08-05 wenzelm 2016-08-05 tuned;
2016-07-20 wenzelm 2016-07-20 moved method "use" to Pure; more documentation;
2016-05-30 matichuk 2016-05-30 apply current morphism to method text before evaluating;
2016-01-13 wenzelm 2016-01-13 tuned signature;
2016-01-12 matichuk 2016-01-12 remove unused code
2016-01-12 matichuk 2016-01-12 remove Eisbach's dependency on HOL
2016-01-11 matichuk 2016-01-11 match method now makes proper use of context_tactic
2015-12-22 wenzelm 2015-12-22 more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
2015-12-15 wenzelm 2015-12-15 tuned signature -- clarified modules;
2015-12-14 wenzelm 2015-12-14 more standard term equality;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-12-12 wenzelm 2015-12-12 tuned;
2015-12-12 wenzelm 2015-12-12 clarified ML scopes; tuned;
2015-12-12 wenzelm 2015-12-12 clarified ML scopes;
2015-12-12 wenzelm 2015-12-12 tuned;
2015-12-12 wenzelm 2015-12-12 unused;
2015-12-12 wenzelm 2015-12-12 tuned;
2015-12-11 wenzelm 2015-12-11 clarified modules;
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 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-08-16 wenzelm 2015-08-16 added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
2015-07-27 wenzelm 2015-07-27 tuned signature; clarified context;
2015-07-26 wenzelm 2015-07-26 updated to infer_instantiate;
2015-07-08 wenzelm 2015-07-08 Variable.focus etc.: optional bindings provided by user; Subgoal.focus command: more careful treatment of user-provided bindings;
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 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-06-03 wenzelm 2015-06-03 clarified context;
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;