Sat, 19 Nov 2005 14:21:00 +0100 wenzelm FOL: -p 2;
Fri, 18 Nov 2005 07:13:58 +0100 chaieb presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
Fri, 18 Nov 2005 07:10:37 +0100 mengj -- changed the interface of functions vampire_oracle and eprover_oracle.
Fri, 18 Nov 2005 07:10:00 +0100 mengj -- terms are fully typed.
Fri, 18 Nov 2005 07:08:54 +0100 mengj -- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
Fri, 18 Nov 2005 07:08:18 +0100 mengj -- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
Fri, 18 Nov 2005 07:07:47 +0100 mengj -- added combinator reduction axioms (typed and untyped) for HOL goals.
Fri, 18 Nov 2005 07:07:06 +0100 mengj -- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
Fri, 18 Nov 2005 07:06:07 +0100 mengj -- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
Fri, 18 Nov 2005 07:05:11 +0100 mengj -- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
Wed, 16 Nov 2005 19:34:19 +0100 wenzelm tuned document;
Wed, 16 Nov 2005 17:50:35 +0100 wenzelm tuned;
Wed, 16 Nov 2005 17:49:16 +0100 wenzelm improved induction proof: local defs/fixes;
Wed, 16 Nov 2005 17:45:36 +0100 wenzelm tuned Pattern.match/unify;
Wed, 16 Nov 2005 17:45:35 +0100 wenzelm added deskolem;
Wed, 16 Nov 2005 17:45:34 +0100 wenzelm added THEN_ALL_NEW_CASES;
Wed, 16 Nov 2005 17:45:33 +0100 wenzelm added revert_skolem, mk_def, add_def;
Wed, 16 Nov 2005 17:45:32 +0100 wenzelm ProofContext.mk_def;
Wed, 16 Nov 2005 17:45:31 +0100 wenzelm Term.betapplys;
Wed, 16 Nov 2005 17:45:30 +0100 wenzelm tuned Pattern.match/unify;
Wed, 16 Nov 2005 17:45:29 +0100 wenzelm added betapplys;
Wed, 16 Nov 2005 17:45:28 +0100 wenzelm tuned interfaces to support incremental match/unify (cf. versions in type.ML);
Wed, 16 Nov 2005 17:45:27 +0100 wenzelm tuned;
Wed, 16 Nov 2005 17:45:26 +0100 wenzelm norm_hhf: no normalization of protected props;
Wed, 16 Nov 2005 17:45:25 +0100 wenzelm added protect_cong, cong_mono_thm;
Wed, 16 Nov 2005 17:45:24 +0100 wenzelm induct: support local definitions to be passed through the induction;
Wed, 16 Nov 2005 17:45:23 +0100 wenzelm Trueprop: use ObjectLogic.judgment etc.;
Wed, 16 Nov 2005 17:45:22 +0100 wenzelm Term.betapply;
Wed, 16 Nov 2005 15:29:23 +0100 paulson new version of "tryres" allowing multiple unifiers (apparently needed for
Wed, 16 Nov 2005 14:05:41 +0100 wenzelm pgmlsymbolson: append Symbol.xsymbolsN at end!
Tue, 15 Nov 2005 14:08:32 +0100 wenzelm better no -d option;
Tue, 15 Nov 2005 10:11:52 +0100 haftmann added generic transformators
Mon, 14 Nov 2005 18:25:34 +0100 paulson removal of is_hol
Mon, 14 Nov 2005 16:26:40 +0100 haftmann added module system
Mon, 14 Nov 2005 15:23:33 +0100 haftmann added modules for code generator generation two, not operational yet
Mon, 14 Nov 2005 15:15:34 +0100 haftmann class_package - operational view on type classes
Mon, 14 Nov 2005 15:15:07 +0100 haftmann string_of_alist - convenient q'n'd printout function
Mon, 14 Nov 2005 15:14:59 +0100 wenzelm support for polyml-4.2.0;
Mon, 14 Nov 2005 15:14:32 +0100 haftmann new syntax for class_package
Mon, 14 Nov 2005 14:37:48 +0100 wenzelm added const_instance;
Mon, 14 Nov 2005 14:37:38 +0100 wenzelm added instance;
Mon, 14 Nov 2005 14:37:15 +0100 wenzelm added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;
Mon, 14 Nov 2005 14:36:46 +0100 wenzelm Compatibility wrapper for Poly/ML 4.2.0.
Mon, 14 Nov 2005 14:36:29 +0100 wenzelm tuned;
Mon, 14 Nov 2005 13:59:58 +0100 urbanc added a few equivariance lemmas (they need to be automated
Sun, 13 Nov 2005 22:36:30 +0100 urbanc changed the HOL_basic_ss back and selectively added
Sun, 13 Nov 2005 20:33:36 +0100 urbanc exchanged HOL_ss for HOL_basic_ss in the simplification
Fri, 11 Nov 2005 10:50:43 +0100 chaieb a proof step corrected due to the changement in the presburger method.
Fri, 11 Nov 2005 10:49:59 +0100 chaieb old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
Fri, 11 Nov 2005 00:09:37 +0100 huffman add header
Thu, 10 Nov 2005 21:14:05 +0100 wenzelm tuned proofs;
Thu, 10 Nov 2005 20:57:22 +0100 wenzelm moved find_free to term.ML;
Thu, 10 Nov 2005 20:57:21 +0100 wenzelm guess: Seq.hd;
Thu, 10 Nov 2005 20:57:20 +0100 wenzelm guess: Toplevel.proof;
Thu, 10 Nov 2005 20:57:19 +0100 wenzelm added find_free (from Isar/proof_context.ML);
Thu, 10 Nov 2005 20:57:18 +0100 wenzelm curried multiply;
Thu, 10 Nov 2005 20:57:17 +0100 wenzelm induct method: fixes;
Thu, 10 Nov 2005 20:57:16 +0100 wenzelm uncurried Consts.typargs;
Thu, 10 Nov 2005 20:57:11 +0100 wenzelm renamed Thm.cgoal_of to Thm.cprem_of;
Thu, 10 Nov 2005 17:33:14 +0100 paulson duplicate axioms in ATP linkup, and general fixes
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip