| Sun, 30 Jul 2006 21:28:52 +0200 |
wenzelm |
Thm.adjust_maxidx;
|
changeset |
files
|
| Sun, 30 Jul 2006 21:28:51 +0200 |
wenzelm |
removed unused add_in_order/add_once (cf. OrdList.insert);
|
changeset |
files
|
| Sun, 30 Jul 2006 21:28:50 +0200 |
wenzelm |
demod_rule: depend on context, proper Variable.import/export;
|
changeset |
files
|
| Sun, 30 Jul 2006 21:28:48 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sun, 30 Jul 2006 05:53:10 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
changeset |
files
|
| Sun, 30 Jul 2006 02:06:01 +0200 |
webertj |
bugfix related to cancel_div_mod simproc
|
changeset |
files
|
| Sat, 29 Jul 2006 13:15:12 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:36 +0200 |
wenzelm |
rename legacy_pretty_thm to pretty_thm_legacy;
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:34 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:33 +0200 |
wenzelm |
added add_fixes_direct;
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:32 +0200 |
wenzelm |
prove: proper assumption context, more tactic arguments;
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:31 +0200 |
wenzelm |
added mk_conjunction_list;
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:29 +0200 |
wenzelm |
Goal.prove: more tactic arguments;
|
changeset |
files
|
| Fri, 28 Jul 2006 18:37:25 +0200 |
paulson |
Checking for unsound proofs. Tidying.
|
changeset |
files
|
| Fri, 28 Jul 2006 18:36:24 +0200 |
paulson |
"all theorems" mode forces definition-expansion off.
|
changeset |
files
|