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;
wenzelm [Tue, 04 Jul 2006 19:49:49 +0200] rev 19998
Thm.varifyT;
wenzelm [Tue, 04 Jul 2006 19:49:47 +0200] rev 19997
added ex/Guess.thy;
wenzelm [Tue, 04 Jul 2006 18:39:59 +0200] rev 19996
skip_proofs: do not skip proofs of schematic goals (warning);