Mon, 16 Jan 2006 21:55:17 +0100 case_result: drop_schematic, i.e. be permissive about illegal binds;
wenzelm [Mon, 16 Jan 2006 21:55:17 +0100] rev 18699
case_result: drop_schematic, i.e. be permissive about illegal binds;
Mon, 16 Jan 2006 21:55:15 +0100 put_facts: do not pretend local thms were named;
wenzelm [Mon, 16 Jan 2006 21:55:15 +0100] rev 18698
put_facts: do not pretend local thms were named;
Mon, 16 Jan 2006 21:55:14 +0100 declare the1_equality [elim?];
wenzelm [Mon, 16 Jan 2006 21:55:14 +0100] rev 18697
declare the1_equality [elim?];
Sun, 15 Jan 2006 20:04:05 +0100 tuned;
wenzelm [Sun, 15 Jan 2006 20:04:05 +0100] rev 18696
tuned;
Sun, 15 Jan 2006 20:00:59 +0100 tuned;
wenzelm [Sun, 15 Jan 2006 20:00:59 +0100] rev 18695
tuned;
Sun, 15 Jan 2006 19:58:57 +0100 * Classical: optional weight for attributes;
wenzelm [Sun, 15 Jan 2006 19:58:57 +0100] rev 18694
* Classical: optional weight for attributes; * HOL: prefer ex1I over ex_ex1I in single-step reasoning;
Sun, 15 Jan 2006 19:58:56 +0100 guess: used fixed inferred_type of vars;
wenzelm [Sun, 15 Jan 2006 19:58:56 +0100] rev 18693
guess: used fixed inferred_type of vars;
Sun, 15 Jan 2006 19:58:55 +0100 export add_args;
wenzelm [Sun, 15 Jan 2006 19:58:55 +0100] rev 18692
export add_args; tuned;
Sun, 15 Jan 2006 19:58:54 +0100 attributes: optional weight;
wenzelm [Sun, 15 Jan 2006 19:58:54 +0100] rev 18691
attributes: optional weight; tuned;
Sun, 15 Jan 2006 19:58:53 +0100 classical attributes: optional weight;
wenzelm [Sun, 15 Jan 2006 19:58:53 +0100] rev 18690
classical attributes: optional weight;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip