Tue, 16 Dec 1997 12:17:22 +0100 |
wenzelm |
improved;
|
changeset |
files
|
Mon, 15 Dec 1997 15:54:47 +0100 |
wenzelm |
improved COMMIT_RO;
|
changeset |
files
|
Mon, 15 Dec 1997 15:32:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 15 Dec 1997 15:27:03 +0100 |
wenzelm |
polyml-3.1;
|
changeset |
files
|
Mon, 15 Dec 1997 15:18:46 +0100 |
wenzelm |
make smlnj-110 default;
|
changeset |
files
|
Mon, 15 Dec 1997 15:16:43 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 15 Dec 1997 14:40:13 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 15 Dec 1997 14:14:06 +0100 |
wenzelm |
No longer depend on theory context!
|
changeset |
files
|
Sat, 13 Dec 1997 17:27:16 +0100 |
wenzelm |
version = "Isabelle98: Jan 1998";
|
changeset |
files
|
Sat, 13 Dec 1997 17:22:41 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
Sat, 13 Dec 1997 17:22:15 +0100 |
wenzelm |
smlnj-110;
|
changeset |
files
|
Fri, 12 Dec 1997 22:43:10 +0100 |
wenzelm |
deleted smlnj-1.09.ML;
|
changeset |
files
|
Fri, 12 Dec 1997 22:41:45 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
Fri, 12 Dec 1997 22:41:15 +0100 |
wenzelm |
Compatibility file for Standard ML of New Jersey.
|
changeset |
files
|
Fri, 12 Dec 1997 22:35:34 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 12 Dec 1997 18:10:59 +0100 |
wenzelm |
prepared for Isabelle98;
|
changeset |
files
|
Fri, 12 Dec 1997 17:51:45 +0100 |
wenzelm |
added;
|
changeset |
files
|
Fri, 12 Dec 1997 17:50:28 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
Fri, 12 Dec 1997 17:23:01 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 12 Dec 1997 17:14:58 +0100 |
wenzelm |
tuned msg;
|
changeset |
files
|
Fri, 12 Dec 1997 17:11:26 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 12 Dec 1997 17:11:05 +0100 |
wenzelm |
major update;
|
changeset |
files
|
Fri, 12 Dec 1997 17:10:40 +0100 |
wenzelm |
SYNC;
|
changeset |
files
|
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
|
Thu, 04 Dec 1997 13:49:51 +0100 |
wenzelm |
added eq_set;
|
changeset |
files
|
Thu, 04 Dec 1997 13:49:27 +0100 |
wenzelm |
moved global_names ref to Pure/ROOT.ML;
|
changeset |
files
|
Thu, 04 Dec 1997 12:50:02 +0100 |
nipkow |
pred -> -1
|
changeset |
files
|
Thu, 04 Dec 1997 12:44:37 +0100 |
nipkow |
pred n -> n-1
|
changeset |
files
|
Thu, 04 Dec 1997 09:05:59 +0100 |
nipkow |
Simplified proofs.
|
changeset |
files
|
Thu, 04 Dec 1997 09:05:39 +0100 |
nipkow |
Added thm mult_div_cancel
|
changeset |
files
|
Wed, 03 Dec 1997 17:31:25 +0100 |
nipkow |
n ~= 0 should become 0 < n
|
changeset |
files
|