Fri, 12 Dec 1997 22:41:15 +0100 wenzelm Compatibility file for Standard ML of New Jersey.
Fri, 12 Dec 1997 22:35:34 +0100 wenzelm tuned;
Fri, 12 Dec 1997 18:10:59 +0100 wenzelm prepared for Isabelle98;
Fri, 12 Dec 1997 17:51:45 +0100 wenzelm added;
Fri, 12 Dec 1997 17:50:28 +0100 wenzelm obsolete;
Fri, 12 Dec 1997 17:23:01 +0100 wenzelm tuned;
Fri, 12 Dec 1997 17:14:58 +0100 wenzelm tuned msg;
Fri, 12 Dec 1997 17:11:26 +0100 wenzelm tuned;
Fri, 12 Dec 1997 17:11:05 +0100 wenzelm major update;
Fri, 12 Dec 1997 17:10:40 +0100 wenzelm SYNC;
Fri, 12 Dec 1997 10:46:09 +0100 paulson new blast_tac no longer works here
Fri, 12 Dec 1997 10:37:45 +0100 paulson More deterministic (?) contr_tac
Fri, 12 Dec 1997 10:34:21 +0100 paulson More deterministic and therefore faster (sometimes) proof reconstruction
Fri, 12 Dec 1997 10:32:45 +0100 paulson ugly patch for new Blast_tac
Fri, 12 Dec 1997 10:31:25 +0100 paulson Faster proof of mult_less_cancel2
Thu, 11 Dec 1997 13:15:06 +0100 wenzelm tuned;
Thu, 11 Dec 1997 10:30:33 +0100 paulson Tidied final proof
Thu, 11 Dec 1997 10:29:22 +0100 paulson Tidied proof of finite_subset_induct
Thu, 11 Dec 1997 10:28:04 +0100 paulson Got rid of mod2_neq_0
Mon, 08 Dec 1997 20:29:49 +0100 wenzelm \subsection{*Theory inclusion};
Mon, 08 Dec 1997 13:57:19 +0100 paulson Tidying to fix overfull lines, etc
Mon, 08 Dec 1997 13:56:49 +0100 paulson Comprehensive (??) list of bugs, fixed or not
Sun, 07 Dec 1997 16:09:55 +0100 wenzelm tuned;
Sun, 07 Dec 1997 16:05:36 +0100 wenzelm added print_claset;
Sat, 06 Dec 1997 17:06:21 +0100 nipkow Replaced Fib(Suc n)~=0 by 0<Fib(Suc(n)).
Sat, 06 Dec 1997 17:05:41 +0100 nipkow Got rid of some preds and replaced some n~=0 by 0<n.
Sat, 06 Dec 1997 16:48:39 +0100 nipkow Cleaned up arithmetic mess.
Fri, 05 Dec 1997 18:46:18 +0100 wenzelm instantiate';
Fri, 05 Dec 1997 18:45:19 +0100 wenzelm changed typed_print_translation;
Fri, 05 Dec 1997 18:44:56 +0100 wenzelm tuned;
Fri, 05 Dec 1997 17:31:01 +0100 wenzelm nat_cancel enabled by default;
Fri, 05 Dec 1997 17:20:25 +0100 wenzelm adapted proofs to cope with simprocs nat_cancel;
Fri, 05 Dec 1997 17:19:38 +0100 wenzelm improved arbitrary_def: we now really don't know nothing about it!
Fri, 05 Dec 1997 17:16:22 +0100 wenzelm use_thy no longer requires writable current directory;
Fri, 05 Dec 1997 17:14:36 +0100 wenzelm adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);
Fri, 05 Dec 1997 17:13:46 +0100 wenzelm simplification procedures nat_cancel enabled by default;
Fri, 05 Dec 1997 08:01:03 +0100 wenzelm tmp_name;
Thu, 04 Dec 1997 14:11:37 +0100 wenzelm added print_simpset;
Thu, 04 Dec 1997 13:50:43 +0100 wenzelm added is_base;
Thu, 04 Dec 1997 13:50:18 +0100 wenzelm added reset_context;
Thu, 04 Dec 1997 13:49:51 +0100 wenzelm added eq_set;
Thu, 04 Dec 1997 13:49:27 +0100 wenzelm moved global_names ref to Pure/ROOT.ML;
Thu, 04 Dec 1997 12:50:02 +0100 nipkow pred -> -1
Thu, 04 Dec 1997 12:44:37 +0100 nipkow pred n -> n-1
Thu, 04 Dec 1997 09:05:59 +0100 nipkow Simplified proofs.
Thu, 04 Dec 1997 09:05:39 +0100 nipkow Added thm mult_div_cancel
Wed, 03 Dec 1997 17:31:25 +0100 nipkow n ~= 0 should become 0 < n
Wed, 03 Dec 1997 17:25:43 +0100 nipkow Replaced n ~= 0 by 0 < n
Wed, 03 Dec 1997 12:55:04 +0100 wenzelm pass return code!!
Wed, 03 Dec 1997 11:42:45 +0100 paulson Fixed the treatment of substitution for equations, restricting occurrences of
Wed, 03 Dec 1997 11:00:24 +0100 paulson updated for latest Blast_tac, which treats equality differently
Wed, 03 Dec 1997 10:52:17 +0100 paulson Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
Wed, 03 Dec 1997 10:50:02 +0100 paulson Tidying and some comments
Wed, 03 Dec 1997 10:49:33 +0100 paulson updated for latest Blast_tac, which treats equality differently
Wed, 03 Dec 1997 10:48:16 +0100 paulson Instantiated the one-point-rule quantifier simpprocs for FOL
Wed, 03 Dec 1997 10:47:13 +0100 paulson updated for latest Blast_tac, which fixes an equality bug
Wed, 03 Dec 1997 10:45:42 +0100 paulson Miniscoping now used except for one proof
Tue, 02 Dec 1997 12:42:59 +0100 wenzelm adapted to new term order;
Tue, 02 Dec 1997 12:42:28 +0100 wenzelm tuned term order;
Tue, 02 Dec 1997 12:41:29 +0100 wenzelm tuned trfuns types;
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip