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;
Tue, 02 Dec 1997 12:41:02 +0100 wenzelm added prod_ord, dict_ord, list_ord;
Tue, 02 Dec 1997 12:40:06 +0100 wenzelm File.tmp_name;
Tue, 02 Dec 1997 12:39:03 +0100 wenzelm added tmp_name;
Tue, 02 Dec 1997 12:38:39 +0100 wenzelm ISABELLE_TMP;
Tue, 02 Dec 1997 12:38:08 +0100 wenzelm added context.ML;
Tue, 02 Dec 1997 12:37:44 +0100 wenzelm Global contexts: session and theory.
Tue, 02 Dec 1997 12:37:22 +0100 wenzelm added Thy/context.ML;
Mon, 01 Dec 1997 18:27:43 +0100 wenzelm open;
Mon, 01 Dec 1997 18:27:06 +0100 wenzelm nat_cancel simprocs;
Mon, 01 Dec 1997 18:22:38 +0100 wenzelm ISABELLE_TMP_PREFIX;
Mon, 01 Dec 1997 18:22:02 +0100 wenzelm ISABELLE_TMP;
Mon, 01 Dec 1997 14:42:30 +0100 berghofe Added DiffCancelSums.
Mon, 01 Dec 1997 12:52:18 +0100 paulson New guarantee B_trusts_NS5, and tidying
Mon, 01 Dec 1997 12:50:04 +0100 paulson speed-up
Mon, 01 Dec 1997 08:59:40 +0100 narasche args for record data
Fri, 28 Nov 1997 16:17:30 +0100 nipkow Removed "open Mutil;"
Fri, 28 Nov 1997 11:00:42 +0100 paulson Added comments
Fri, 28 Nov 1997 10:59:14 +0100 paulson New timing functions startTiming and endTiming
Fri, 28 Nov 1997 10:54:13 +0100 paulson addsplits now in FOL, ZF too
Fri, 28 Nov 1997 10:52:32 +0100 paulson New example
Fri, 28 Nov 1997 10:52:04 +0100 paulson Printing of statistics including time for search & reconstruction
Fri, 28 Nov 1997 10:36:08 +0100 paulson New example
Fri, 28 Nov 1997 07:41:24 +0100 nipkow Removed dead code.
Fri, 28 Nov 1997 07:37:06 +0100 nipkow Moved the quantifier elimination simp procs into Provers.
Fri, 28 Nov 1997 07:35:47 +0100 nipkow Quantifier elimination procs.
Fri, 28 Nov 1997 07:35:10 +0100 nipkow Fixed the definition of `termord': is now antisymmetric.
Thu, 27 Nov 1997 19:39:02 +0100 wenzelm several minor updates;
Thu, 27 Nov 1997 19:37:36 +0100 wenzelm SYNC;
Thu, 27 Nov 1997 19:36:51 +0100 wenzelm removed read_cterms;
Thu, 27 Nov 1997 19:36:31 +0100 wenzelm fixed warning;
Thu, 27 Nov 1997 19:36:08 +0100 wenzelm removed same_thm;
Thu, 27 Nov 1997 14:05:25 +0100 paulson Tidying, mostly indentation
Thu, 27 Nov 1997 13:58:51 +0100 paulson Deleted some needless addSIs; got rid of a slow Blast_tac
Thu, 27 Nov 1997 13:38:06 +0100 wenzelm mk_norm_sum;
Wed, 26 Nov 1997 17:52:53 +0100 wenzelm separate lists of simprocs;
Wed, 26 Nov 1997 17:35:46 +0100 paulson Added rule impCE'
Wed, 26 Nov 1997 17:35:08 +0100 paulson Blast_tac can prove Pelletier\'s problem 46\!
Wed, 26 Nov 1997 17:32:52 +0100 paulson Tidying and using equalityCE instead of the slower equalityE
Wed, 26 Nov 1997 17:31:02 +0100 paulson The change from iffE to iffCE means fewer case splits in most cases. Very few
Wed, 26 Nov 1997 17:27:34 +0100 paulson Tidying
Wed, 26 Nov 1997 17:26:12 +0100 paulson Tidying and modification to cope with iffCE
Wed, 26 Nov 1997 17:23:18 +0100 paulson Added rule impCE'
Wed, 26 Nov 1997 17:16:48 +0100 paulson Changes to AddIs improve performance of Blast_tac
Wed, 26 Nov 1997 16:49:54 +0100 paulson Statistics
Wed, 26 Nov 1997 16:49:07 +0100 paulson updated comment
Wed, 26 Nov 1997 16:48:11 +0100 paulson Tidying and modification to cope with iffCE
Wed, 26 Nov 1997 16:45:54 +0100 wenzelm added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
Wed, 26 Nov 1997 16:44:47 +0100 wenzelm added Arith provers;
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip