wenzelm [Tue, 04 Jul 2006 19:49:59 +0200] rev 20008
add_abbrevs/polymorphic: Variable.exportT_terms avoids over-generalization;
wenzelm [Tue, 04 Jul 2006 19:49:58 +0200] rev 20007
instantiate_tfrees: Thm.generalize;
wenzelm [Tue, 04 Jul 2006 19:49:57 +0200] rev 20006
removed parrot comment;
wenzelm [Tue, 04 Jul 2006 19:49:56 +0200] rev 20005
Proof by guessing.
wenzelm [Tue, 04 Jul 2006 19:49:55 +0200] rev 20004
guess: proper context for polymorphic parameters;
tuned;
wenzelm [Tue, 04 Jul 2006 19:49:54 +0200] rev 20003
polymorphic: always generalize wrt. used_types;
wenzelm [Tue, 04 Jul 2006 19:49:53 +0200] rev 20002
varifyT: no longer pervasive;
wenzelm [Tue, 04 Jul 2006 19:49:52 +0200] rev 20001
added generalize/instantiate_option;
wenzelm [Tue, 04 Jul 2006 19:49:51 +0200] rev 20000
added map_proof_terms_option;
tuned generalize, instantiate;
wenzelm [Tue, 04 Jul 2006 19:49:50 +0200] rev 19999
added generalize;
removed obsolete assume_ax, tvars_intr_list;