src/Pure/Tools/find_theorems.ML
2014-12-04 ago eta-expand all search patterns using schematic place holders
2014-12-04 ago revert "better" handling of abbreviation from c61fe520602b
2014-12-04 ago tuned variable names
2014-12-04 ago turn application-specific Pattern.matches_subterm into an application-private function
2014-12-03 ago tuned signature;
2014-11-26 ago renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-07 ago plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
2014-11-06 ago tuned signature;
2014-11-05 ago more frugal keywords;
2014-11-05 ago explicit type Keyword.keywords;
2014-11-03 ago eliminated unused int_only flag (see also c12484a27367);
2014-10-30 ago eliminated aliases;
2014-08-12 ago tuned signature according to Scala version -- prefer explicit argument;
2014-07-25 ago tuned comment;
2014-05-08 ago tuned message;
2014-05-08 ago some position markup to help locating the query context, e.g. from "Info" dockable;
2014-05-08 ago tuned message: more compact, imitate actual command line;
2014-05-07 ago tuned message -- more context for detached window etc.;
2014-04-19 ago removed odd context argument: Thy_Info.get_theory does not fit into PIDE document model;
2014-04-17 ago tuned option name;
2014-04-08 ago more uniform ML/document antiquotations;
2014-03-15 ago clarified local facts;
2014-03-15 ago more explicit treatment of verbose mode, which includes concealed entries;
2014-03-14 ago more accurate resolution of hybrid facts, which actually changes the sort order of results;
2014-03-14 ago back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
2014-03-14 ago just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
2014-03-10 ago more direct Long_Name.qualification;
2014-02-22 ago support for completion within the formal context;
2014-02-22 ago removed remains of old experiment (see b933142e02d0);
2014-02-22 ago removed dead code;
2014-02-22 ago tuned signature;
2013-12-14 ago proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
2013-09-14 ago print find_thms result in reverse order so best result is on top
2013-09-14 ago more useful sorting of find_thms results
2013-08-12 ago clarified Query_Operation.register: avoid hard-wired parallel policy;
2013-08-10 ago prefer local facts over global ones
2013-08-10 ago use local context for name space
2013-08-09 ago enable search in pre-loaded theory;
2013-08-09 ago more GUI options;
2013-08-09 ago tuned signature;
2013-08-09 ago tuned;
2013-08-09 ago more explicit error;
2013-08-09 ago tuned message;
2013-08-08 ago removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
2013-08-08 ago more robust read_query;
2013-08-05 ago slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
2013-08-05 ago more message markup, provided by prover;
2013-08-02 ago some actual find_theorems functionality;
2013-08-02 ago more general Output.result: allow to update arbitrary properties;
2013-08-02 ago minimal print function "find_theorems", which merely echos its arguments;
2013-07-30 ago type theory is purely value-oriented;
2013-07-18 ago modify background theory where it is actually required (cf. 51dfdcd88e84);
2013-07-18 ago tuned messages -- avoid text folds stemming from Pretty.chunks;
2013-07-18 ago proper system options for 'find_theorems';
2013-07-18 ago guard unify tracing via visible status of global theory;
2013-04-18 ago simplifier uses proper Proof.context instead of historic type simpset;
2013-04-09 ago discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
2012-11-26 ago clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
2012-11-26 ago tuned command descriptions;
2012-10-17 ago more formal markup;