src/Pure/Isar/find_theorems.ML
2007-04-15 wenzelm 2007-04-15 removed obsolete TypeInfer.logicT -- use dummyT;
2007-03-06 kleing 2007-03-06 an O(n log n) version of removing duplicates
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-21 kleing 2007-02-21 prevent quadratic time removal of duplicates if filter list is empty (likely to have too many results)
2007-02-20 kleing 2007-02-20 Remove duplicates from printed theorems in find_theorems (still pretty slow, needs optimising). Added syntax "find_theorems (..) with_dups .." to switch off removal.
2006-04-29 wenzelm 2006-04-29 tuned;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 *** empty log message ***
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-06 wenzelm 2006-02-06 tuned;
2005-12-01 wenzelm 2005-12-01 ProofContext.lthms_containing: suppress obvious duplicates;
2005-11-16 wenzelm 2005-11-16 tuned Pattern.match/unify;
2005-10-21 wenzelm 2005-10-21 do not export find_thms;
2005-10-07 wenzelm 2005-10-07 removed obsolete comment;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-10-04 wenzelm 2005-10-04 find_theorems: support * wildcard in name: criterion;
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig; use Thm.full_prop_of instead of Thm.prop_of; tuned use of map/filter/fold;
2005-08-18 wenzelm 2005-08-18 use theory instead of obsolete Sign.sg; tuned comments;
2005-08-01 kleing 2005-08-01 Ordering is now: first by number of assumptions, second by the substitution size. Treat elim/dest rules like erule/drule would: * "elim" is now a subset of "dest" and matches on conclusion of goal and major premise against any premise of goal. Computed substitution size takes both into account. * "dest" no longer has a restriction that limits its conclusion to a var. (contributed by Raf)
2005-07-20 kleing 2005-07-20 Sort search results in order of relevance, where relevance = a) better if 0 premises for intro or 1 premise for elim/dest rules b) better if substitution size wrt to current goal is smaller Only applies to intro, dest, elim, and simp (contributed by Rafal Kolanski, NICTA)
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-05-26 kleing 2005-05-26 cleaned up select_match do not return trivial matches made simp: t work
2005-05-25 kleing 2005-05-25 more cleanup
2005-05-25 kleing 2005-05-25 renamed search criterion 'rewrite' to 'simp'
2005-05-25 kleing 2005-05-25 removed obsolete findI, findE, findEs (and the functions they depended on in Isar/find_theorems)
2005-05-22 wenzelm 2005-05-22 added read_criterion/pretty_criterion; improved rule filters -- intro excludes elim rules; tuned output; tuned;
2005-05-22 wenzelm 2005-05-22 Retrieve theorems from proof context -- improved version of thms_containing by Rafal Kolanski, NICTA;