| Fri, 12 Dec 1997 10:46:09 +0100 |
paulson |
new blast_tac no longer works here
|
changeset |
files
|
| Fri, 12 Dec 1997 10:37:45 +0100 |
paulson |
More deterministic (?) contr_tac
|
changeset |
files
|
| Fri, 12 Dec 1997 10:34:21 +0100 |
paulson |
More deterministic and therefore faster (sometimes) proof reconstruction
|
changeset |
files
|
| Fri, 12 Dec 1997 10:32:45 +0100 |
paulson |
ugly patch for new Blast_tac
|
changeset |
files
|
| Fri, 12 Dec 1997 10:31:25 +0100 |
paulson |
Faster proof of mult_less_cancel2
|
changeset |
files
|
| Thu, 11 Dec 1997 13:15:06 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Dec 1997 10:30:33 +0100 |
paulson |
Tidied final proof
|
changeset |
files
|
| Thu, 11 Dec 1997 10:29:22 +0100 |
paulson |
Tidied proof of finite_subset_induct
|
changeset |
files
|
| Thu, 11 Dec 1997 10:28:04 +0100 |
paulson |
Got rid of mod2_neq_0
|
changeset |
files
|
| Mon, 08 Dec 1997 20:29:49 +0100 |
wenzelm |
\subsection{*Theory inclusion};
|
changeset |
files
|
| Mon, 08 Dec 1997 13:57:19 +0100 |
paulson |
Tidying to fix overfull lines, etc
|
changeset |
files
|
| Mon, 08 Dec 1997 13:56:49 +0100 |
paulson |
Comprehensive (??) list of bugs, fixed or not
|
changeset |
files
|
| Sun, 07 Dec 1997 16:09:55 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 07 Dec 1997 16:05:36 +0100 |
wenzelm |
added print_claset;
|
changeset |
files
|
| Sat, 06 Dec 1997 17:06:21 +0100 |
nipkow |
Replaced Fib(Suc n)~=0 by 0<Fib(Suc(n)).
|
changeset |
files
|
| Sat, 06 Dec 1997 17:05:41 +0100 |
nipkow |
Got rid of some preds and replaced some n~=0 by 0<n.
|
changeset |
files
|
| Sat, 06 Dec 1997 16:48:39 +0100 |
nipkow |
Cleaned up arithmetic mess.
|
changeset |
files
|
| Fri, 05 Dec 1997 18:46:18 +0100 |
wenzelm |
instantiate';
|
changeset |
files
|
| Fri, 05 Dec 1997 18:45:19 +0100 |
wenzelm |
changed typed_print_translation;
|
changeset |
files
|
| Fri, 05 Dec 1997 18:44:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 05 Dec 1997 17:31:01 +0100 |
wenzelm |
nat_cancel enabled by default;
|
changeset |
files
|
| Fri, 05 Dec 1997 17:20:25 +0100 |
wenzelm |
adapted proofs to cope with simprocs nat_cancel;
|
changeset |
files
|
| Fri, 05 Dec 1997 17:19:38 +0100 |
wenzelm |
improved arbitrary_def: we now really don't know nothing about it!
|
changeset |
files
|
| Fri, 05 Dec 1997 17:16:22 +0100 |
wenzelm |
use_thy no longer requires writable current directory;
|
changeset |
files
|
| Fri, 05 Dec 1997 17:14:36 +0100 |
wenzelm |
adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);
|
changeset |
files
|
| Fri, 05 Dec 1997 17:13:46 +0100 |
wenzelm |
simplification procedures nat_cancel enabled by default;
|
changeset |
files
|
| Fri, 05 Dec 1997 08:01:03 +0100 |
wenzelm |
tmp_name;
|
changeset |
files
|
| Thu, 04 Dec 1997 14:11:37 +0100 |
wenzelm |
added print_simpset;
|
changeset |
files
|
| Thu, 04 Dec 1997 13:50:43 +0100 |
wenzelm |
added is_base;
|
changeset |
files
|
| Thu, 04 Dec 1997 13:50:18 +0100 |
wenzelm |
added reset_context;
|
changeset |
files
|