src/Pure/Tools/find_theorems.ML
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;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-21 kleing 2009-10-21 find_theorems: better handling of abbreviations (by Timothy Bourke)
2009-10-20 wenzelm 2009-10-20 uniform use of Integer.min/max;
2009-10-02 wenzelm 2009-10-02 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-10-01 wenzelm 2009-10-01 misc tuning and simplification; be explicit about expressions involving infixes with non-obvious priorities; removed dead code; some attempts to recover basic Isabelle coding conventions;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-17 wenzelm 2009-06-17 more detailed start_timing/end_timing;
2009-06-17 wenzelm 2009-06-17 minor tuning according to Isabelle/ML conventions; slightly less combinators;
2009-05-06 Timothy Bourke 2009-05-06 Prototype introiff option for find_theorems. This feature was suggested by Jeremy Avigad / Tobias Nipkow. It adds an introiff keyword for find_theorems that returns, in addition to the usual results for intro, any theorems of the form ([| ... |] ==> (P = Q)) where either P or Q matches the conclusions of the current goal. Such theorems can be made introduction rules with [THEN iffDx]. The current patch is for evaluation only. It assumes an (op = : 'a -> 'a -> bool) operator, which is specific to HOL. It is not clear how this should be generalised.
2009-03-31 wenzelm 2009-03-31 superficial tuning;
2009-03-30 Timothy Bourke 2009-03-30 Limit the number of results returned by auto_solves.
2009-03-24 Timothy Bourke 2009-03-24 Use assms rather than prems in find_theorems solves.
2009-03-12 wenzelm 2009-03-12 Assumption.all_prems_of, Assumption.all_assms_of;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-06 wenzelm 2009-03-06 replaced archaic use of rep_ss by Simplifier.mksimps;
2009-03-04 wenzelm 2009-03-04 renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
2009-03-03 wenzelm 2009-03-03 nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
2009-03-01 wenzelm 2009-03-01 avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
2009-03-01 wenzelm 2009-03-01 replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already); minor tuning according to Isabelle coding conventions;
2009-02-27 wenzelm 2009-02-27 observe basic Isabelle/ML coding conventions;
2009-02-27 wenzelm 2009-02-27 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;