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;
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;