src/Pure/Isar/method.ML
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-04-01 wenzelm 2016-04-01 removed redundant Position.set_range -- already done in Position.range;
2015-12-23 wenzelm 2015-12-23 check and report source at most once, notably in body of "match" method;
2015-12-14 wenzelm 2015-12-14 tuned message;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-12-11 wenzelm 2015-12-11 clarified modules;
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-12-08 wenzelm 2015-12-08 tuned;
2015-10-18 wenzelm 2015-10-18 tuned signature;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-13 wenzelm 2015-09-13 renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-09-13 wenzelm 2015-09-13 method "goals" ignores facts;
2015-08-30 wenzelm 2015-08-30 trim context for persistent storage;
2015-06-30 wenzelm 2015-06-30 renamed "default" to "standard", to make semantically clear what it is;
2015-06-29 wenzelm 2015-06-29 clarified static phase; proper error;
2015-06-25 wenzelm 2015-06-25 added method "goals" for proper subgoal cases;
2015-06-22 wenzelm 2015-06-22 added method "sleep";
2015-06-22 wenzelm 2015-06-22 tuned signature;
2015-05-01 wenzelm 2015-05-01 clarified markup range;
2015-05-01 wenzelm 2015-05-01 modifier markup for all parsed tokens; report literal token markup, before re-assignment;
2015-04-09 wenzelm 2015-04-09 option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
2015-04-09 wenzelm 2015-04-09 tuned signature;
2015-04-08 wenzelm 2015-04-08 tuned signature;
2015-04-03 wenzelm 2015-04-03 more uniform "verbose" option to print name space;
2015-04-02 wenzelm 2015-04-02 proper treatment of internal method name as already checked Token.src;
2015-04-02 wenzelm 2015-04-02 clarified method_closure; added option for Eisbach, which makes its own closure;
2015-04-02 wenzelm 2015-04-02 tuned signature;
2015-03-10 wenzelm 2015-03-10 clarified Token.check_src: intern at most once; Method.parse_internal for Eisbach: intern method names;
2015-03-09 wenzelm 2015-03-09 support structural composition (THEN_ALL_NEW) for proof methods; clarified preparation for goal restriction: Goal.conjunction_tac only once; export Method.parse0, notably for Eisbach; more explicit type cases_state;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-30 wenzelm 2014-11-30 tuned signature;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
2014-11-12 wenzelm 2014-11-12 more careful ML source positions, for improved PIDE markup;
2014-11-11 wenzelm 2014-11-11 more careful ML source positions, for improved PIDE markup;
2014-11-11 wenzelm 2014-11-11 more position information, e.g. relevant for errors in generated ML source;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-08-28 wenzelm 2014-08-28 intern xthm only once;
2014-08-27 wenzelm 2014-08-27 more explicit Method.modifier with reported position;
2014-08-22 wenzelm 2014-08-22 attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";
2014-08-22 wenzelm 2014-08-22 made SML/NJ happy;
2014-08-21 wenzelm 2014-08-21 clarified Method.section: explicit declaration with static closure;
2014-08-21 wenzelm 2014-08-21 tuned;
2014-08-21 wenzelm 2014-08-21 tuned;
2014-08-20 wenzelm 2014-08-20 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
2014-08-20 wenzelm 2014-08-20 more uniform data slot;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-08-19 wenzelm 2014-08-19 just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
2014-08-19 wenzelm 2014-08-19 tuned signature;
2014-08-19 wenzelm 2014-08-19 more compact datatypes;
2014-08-19 wenzelm 2014-08-19 tuned;
2014-08-19 wenzelm 2014-08-19 clarifed Method.evaluate: turn text into semantic method (like Basic);
2014-08-19 wenzelm 2014-08-19 simplified type Proof.method;
2014-08-14 wenzelm 2014-08-14 localized command 'method_setup' and 'attribute_setup'; clarified (non)application of morphism: argument src is already transformed, semantic body remains untransformed;
2014-08-14 wenzelm 2014-08-14 tuned;
2014-08-14 wenzelm 2014-08-14 tuned;
2014-08-14 wenzelm 2014-08-14 localized method definitions (see also f14c1248d064);
2014-08-05 wenzelm 2014-08-05 avoid duplication of warnings stemming from simp/intro declarations etc.;