20070415 
wenzelm 
20070415 
removed obsolete TypeInfer.logicT  use dummyT;

file  diff  annotate 
20070306 
kleing 
20070306 
an O(n log n) version of removing duplicates

file  diff  annotate 
20070226 
wenzelm 
20070226 
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;

file  diff  annotate 
20070221 
kleing 
20070221 
prevent quadratic time removal of duplicates if filter list is empty (likely to have too many results)

file  diff  annotate 
20070220 
kleing 
20070220 
Remove duplicates from printed theorems in find_theorems
(still pretty slow, needs optimising).
Added syntax "find_theorems (..) with_dups .." to switch off removal.

file  diff  annotate 
20060429 
wenzelm 
20060429 
tuned;

file  diff  annotate 
20060427 
wenzelm 
20060427 
tuned basic list operators (flat, maps, map_filter);

file  diff  annotate 
20060426 
wenzelm 
20060426 
*** empty log message ***

file  diff  annotate 
20060215 
wenzelm 
20060215 
removed distinct, renamed gen_distinct to distinct;

file  diff  annotate 
20060206 
wenzelm 
20060206 
tuned;

file  diff  annotate 
20051201 
wenzelm 
20051201 
ProofContext.lthms_containing: suppress obvious duplicates;

file  diff  annotate 
20051116 
wenzelm 
20051116 
tuned Pattern.match/unify;

file  diff  annotate 
20051021 
wenzelm 
20051021 
do not export find_thms;

file  diff  annotate 
20051007 
wenzelm 
20051007 
removed obsolete comment;

file  diff  annotate 
20051004 
wenzelm 
20051004 
minor tweaks for Poplog/ML;

file  diff  annotate 
20051004 
wenzelm 
20051004 
find_theorems: support * wildcard in name: criterion;

file  diff  annotate 
20050831 
wenzelm 
20050831 
refer to theory instead of lowlevel tsig;
use Thm.full_prop_of instead of Thm.prop_of;
tuned use of map/filter/fold;

file  diff  annotate 
20050818 
wenzelm 
20050818 
use theory instead of obsolete Sign.sg;
tuned comments;

file  diff  annotate 
20050801 
kleing 
20050801 
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)

file  diff  annotate 
20050720 
kleing 
20050720 
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)

file  diff  annotate 
20050620 
wenzelm 
20050620 
get_thm(s): Name;

file  diff  annotate 
20050526 
kleing 
20050526 
cleaned up select_match
do not return trivial matches
made simp: t work

file  diff  annotate 
20050525 
kleing 
20050525 
more cleanup

file  diff  annotate 
20050525 
kleing 
20050525 
renamed search criterion 'rewrite' to 'simp'

file  diff  annotate 
20050525 
kleing 
20050525 
removed obsolete findI, findE, findEs
(and the functions they depended on in Isar/find_theorems)

file  diff  annotate 
20050522 
wenzelm 
20050522 
added read_criterion/pretty_criterion;
improved rule filters  intro excludes elim rules;
tuned output;
tuned;

file  diff  annotate 
20050522 
wenzelm 
20050522 
Retrieve theorems from proof context  improved version of
thms_containing by Rafal Kolanski, NICTA;

file  diff  annotate 