src/Pure/Tools/find_theorems.ML
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;
2011-07-10 wenzelm 2011-07-10 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); tuned signature;
2011-07-10 wenzelm 2011-07-10 simplified XML_Data;
2011-07-01 wenzelm 2011-07-01 tuned layout;
2011-05-30 krauss 2011-05-30 parameterize print_theorems over actual search function
2011-05-30 krauss 2011-05-30 (de)serialization for search query and result
2011-05-30 krauss 2011-05-30 explicit type for search queries
2011-05-30 krauss 2011-05-30 moved questionable goal modification out of filter_theorems
2011-05-30 krauss 2011-05-30 exported raw query parser; removed inconsistent clone
2011-05-30 krauss 2011-05-30 separate query parsing from actual search
2011-05-03 wenzelm 2011-05-03 more conventional naming scheme: names_long, names_short, names_unique;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
2011-02-25 krauss 2011-02-25 reactivate time measurement (partly reverting c27b0b37041a); export pretty_theorem, to display both internal or external facts
2011-02-25 krauss 2011-02-25 generalize find_theorems filters to work on raw propositions, too
2011-02-25 noschinl 2011-02-25 Refactor find_theorems to provide a more general filter_facts method
2011-02-23 noschinl 2011-02-23 fix non-exhaustive pattern match in find_theorems
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-11 wenzelm 2010-08-11 misc tuning and simplification;
2010-08-11 wenzelm 2010-08-11 simplified/unified command setup;
2010-05-15 wenzelm 2010-05-15 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-12-14 haftmann 2009-12-14 avoid negative indices as argument ot drop
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-29 kleing 2009-11-29 Expand nested abbreviations before applying dummy patterns.
2009-11-02 wenzelm 2009-11-02 observe usual naming conventions;
2009-11-02 krauss 2009-11-02 find_theorems: respect conceal flag
2009-10-29 wenzelm 2009-10-29 less hermetic ML; parse_pattern: apply Consts.intern only once (Why is this done anyway?); modernized structure names;
2009-10-28 wenzelm 2009-10-28 renamed Proof.flat_goal to Proof.simple_goal;