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 