src/Pure/Tools/find_theorems.ML
2016-07-10 wenzelm 2016-07-10 tuned signature: more uniform Keyword.spec;
2016-05-10 wenzelm 2016-05-10 find dynamic facts as well, but static ones are preferred; tuned;
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-04-04 wenzelm 2016-04-04 clarified bootstrap -- more uniform use of ML files;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-21 wenzelm 2015-09-21 clarified markup; tuned signature;
2015-08-30 wenzelm 2015-08-30 trim context for persistent storage;
2015-06-29 wenzelm 2015-06-29 improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-04-06 wenzelm 2015-04-06 more position information and PIDE markup for command keywords;
2015-04-03 wenzelm 2015-04-03 tuned;
2015-04-01 wenzelm 2015-04-01 tuned signature;
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-12-04 haftmann 2014-12-04 eta-expand all search patterns using schematic place holders
2014-12-04 haftmann 2014-12-04 revert "better" handling of abbreviation from c61fe520602b
2014-12-04 haftmann 2014-12-04 tuned variable names
2014-12-04 haftmann 2014-12-04 turn application-specific Pattern.matches_subterm into an application-private function
2014-12-03 wenzelm 2014-12-03 tuned signature;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-06 wenzelm 2014-11-06 tuned signature;
2014-11-05 wenzelm 2014-11-05 more frugal keywords;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-08-12 wenzelm 2014-08-12 tuned signature according to Scala version -- prefer explicit argument;
2014-07-25 wenzelm 2014-07-25 tuned comment;
2014-05-08 wenzelm 2014-05-08 tuned message;
2014-05-08 wenzelm 2014-05-08 some position markup to help locating the query context, e.g. from "Info" dockable;
2014-05-08 wenzelm 2014-05-08 tuned message: more compact, imitate actual command line;
2014-05-07 wenzelm 2014-05-07 tuned message -- more context for detached window etc.;
2014-04-19 wenzelm 2014-04-19 removed odd context argument: Thy_Info.get_theory does not fit into PIDE document model;
2014-04-17 wenzelm 2014-04-17 tuned option name;
2014-04-08 wenzelm 2014-04-08 more uniform ML/document antiquotations;
2014-03-15 wenzelm 2014-03-15 clarified local facts;
2014-03-15 wenzelm 2014-03-15 more explicit treatment of verbose mode, which includes concealed entries;
2014-03-14 wenzelm 2014-03-14 more accurate resolution of hybrid facts, which actually changes the sort order of results;
2014-03-14 wenzelm 2014-03-14 back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
2014-03-14 wenzelm 2014-03-14 just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.); more thorough background_notes: distribute global notes to all contexts;
2014-03-10 wenzelm 2014-03-10 more direct Long_Name.qualification;
2014-02-22 wenzelm 2014-02-22 support for completion within the formal context; tuned signature;
2014-02-22 wenzelm 2014-02-22 removed remains of old experiment (see b933142e02d0);
2014-02-22 wenzelm 2014-02-22 removed dead code; more complete patterns;
2014-02-22 wenzelm 2014-02-22 tuned signature;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-09-14 kleing 2013-09-14 print find_thms result in reverse order so best result is on top
2013-09-14 kleing 2013-09-14 more useful sorting of find_thms results
2013-08-12 wenzelm 2013-08-12 clarified Query_Operation.register: avoid hard-wired parallel policy; sledgehammer: more conventional parallel exception handling -- print just one interrupt;
2013-08-10 kleing 2013-08-10 prefer local facts over global ones
2013-08-10 kleing 2013-08-10 use local context for name space
2013-08-09 wenzelm 2013-08-09 enable search in pre-loaded theory;
2013-08-09 wenzelm 2013-08-09 more GUI options;
2013-08-09 wenzelm 2013-08-09 tuned signature;
2013-08-09 wenzelm 2013-08-09 tuned;
2013-08-09 wenzelm 2013-08-09 more explicit error;
2013-08-09 wenzelm 2013-08-09 tuned message;
2013-08-08 wenzelm 2013-08-08 removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
2013-08-08 wenzelm 2013-08-08 more robust read_query; avoid pointless position, which is always line 1 for single-line input;