src/Pure/Tools/find_theorems.ML
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;
2013-08-05 wenzelm 2013-08-05 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
2013-08-05 wenzelm 2013-08-05 more message markup, provided by prover;
2013-08-02 wenzelm 2013-08-02 some actual find_theorems functionality;
2013-08-02 wenzelm 2013-08-02 more general Output.result: allow to update arbitrary properties; clarified kind/instance of overlay GUI component, with separate output (subject to version as main Output);
2013-08-02 wenzelm 2013-08-02 minimal print function "find_theorems", which merely echos its arguments;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-07-18 wenzelm 2013-07-18 modify background theory where it is actually required (cf. 51dfdcd88e84);
2013-07-18 wenzelm 2013-07-18 tuned messages -- avoid text folds stemming from Pretty.chunks;
2013-07-18 wenzelm 2013-07-18 proper system options for 'find_theorems';
2013-07-18 wenzelm 2013-07-18 guard unify tracing via visible status of global theory; find_theorems: back-patching of background theory to observe Context_Position.is_visible avoids spamming via auto solve_direct;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-09 wenzelm 2013-04-09 discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;
2012-11-26 wenzelm 2012-11-26 clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
2012-11-26 wenzelm 2012-11-26 tuned command descriptions;
2012-10-17 wenzelm 2012-10-17 more formal markup;
2012-08-02 wenzelm 2012-08-02 more official command specifications, including source position;
2012-03-17 wenzelm 2012-03-17 slightly more parallel find_theorems;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-02-27 wenzelm 2012-02-27 tuned;
2012-02-27 wenzelm 2012-02-27 removed broken/unused introiff (cf. d452117ba564);
2012-02-27 wenzelm 2012-02-27 discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
2012-02-27 wenzelm 2012-02-27 prefer uniform Timing.message -- avoid assumption about sequential execution;
2011-07-12 wenzelm 2011-07-12 tuned XML modules;