src/Pure/Tools/find_theorems.ML
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;