Fri, 25 Nov 2005 18:58:38 +0100 wenzelm tuned names;
Fri, 25 Nov 2005 18:58:37 +0100 wenzelm forall_conv: limit prefix;
Fri, 25 Nov 2005 18:58:36 +0100 wenzelm fix_tac: proper treatment of major premises in goal;
Fri, 25 Nov 2005 18:58:35 +0100 wenzelm removed obsolete dummy paragraphs;
Fri, 25 Nov 2005 18:58:34 +0100 wenzelm tuned;
Fri, 25 Nov 2005 17:41:52 +0100 haftmann code generator: case expressions, improved name resolving
Fri, 25 Nov 2005 14:51:39 +0100 urbanc added fsub.thy (poplmark challenge) to the examples
Fri, 25 Nov 2005 14:00:22 +0100 berghofe Fixed problem with strong induction theorem for datatypes containing
Fri, 25 Nov 2005 11:34:37 +0100 kleing send more information with test-takes-too-long message
Thu, 24 Nov 2005 12:14:56 +0100 wenzelm fixed spelling of 'case_conclusion';
Thu, 24 Nov 2005 00:00:20 +0100 wenzelm tuned induct proofs;
Wed, 23 Nov 2005 22:26:13 +0100 wenzelm tuned induction proofs;
Wed, 23 Nov 2005 22:23:52 +0100 wenzelm more robust revert_skolem;
Wed, 23 Nov 2005 20:29:36 +0100 wenzelm tuned;
Wed, 23 Nov 2005 18:52:05 +0100 wenzelm Provers/induct: definitional insts and fixing;
Wed, 23 Nov 2005 18:52:04 +0100 wenzelm consume: proper treatment of defs;
Wed, 23 Nov 2005 18:52:03 +0100 wenzelm added case_conclusion attribute;
Wed, 23 Nov 2005 18:52:02 +0100 wenzelm (co)induct: taking;
Wed, 23 Nov 2005 18:52:01 +0100 wenzelm RuleCases.case_conclusion;
Wed, 23 Nov 2005 18:52:00 +0100 wenzelm tuned;
Wed, 23 Nov 2005 18:51:59 +0100 wenzelm added case_conclusion attribute;
Wed, 23 Nov 2005 17:16:42 +0100 haftmann improved failure tracking
Tue, 22 Nov 2005 19:37:36 +0100 wenzelm Datatype_Universe: hide base names only;
Tue, 22 Nov 2005 19:34:50 +0100 wenzelm added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
Tue, 22 Nov 2005 19:34:48 +0100 wenzelm cases_tactic;
Tue, 22 Nov 2005 19:34:47 +0100 wenzelm moved multi_resolve(s) to drule.ML;
Tue, 22 Nov 2005 19:34:46 +0100 wenzelm find_xxxS: term instead of thm;
Tue, 22 Nov 2005 19:34:44 +0100 wenzelm export map_tags;
Tue, 22 Nov 2005 19:34:43 +0100 wenzelm make coinduct actually work;
Tue, 22 Nov 2005 19:34:41 +0100 wenzelm Drule.multi_resolves;
Tue, 22 Nov 2005 19:34:40 +0100 wenzelm declare coinduct rule;
Tue, 22 Nov 2005 14:32:01 +0100 haftmann added code generator syntax
Tue, 22 Nov 2005 12:59:25 +0100 haftmann added codegenerator
Tue, 22 Nov 2005 12:42:59 +0100 haftmann added code generator syntax
Tue, 22 Nov 2005 10:09:11 +0100 paulson new treatment of polymorphic types, using Sign.const_typargs
Mon, 21 Nov 2005 16:51:57 +0100 haftmann added codegen package
Mon, 21 Nov 2005 15:15:32 +0100 haftmann added serializer
Mon, 21 Nov 2005 11:14:11 +0100 paulson tweak
Mon, 21 Nov 2005 10:44:14 +0100 haftmann fixed some inconveniencies in website
Sat, 19 Nov 2005 14:22:28 +0100 wenzelm CONJUNCTS;
Sat, 19 Nov 2005 14:21:09 +0100 wenzelm tuned;
Sat, 19 Nov 2005 14:21:08 +0100 wenzelm Goal.norm_hhf_protected;
Sat, 19 Nov 2005 14:21:07 +0100 wenzelm added coinduct attribute;
Sat, 19 Nov 2005 14:21:06 +0100 wenzelm added CONJUNCTS: treat conjunction as separate sub-goals;
Sat, 19 Nov 2005 14:21:05 +0100 wenzelm simpset: added reorient field, set_reorient;
Sat, 19 Nov 2005 14:21:04 +0100 wenzelm tuned norm_hhf_protected;
Sat, 19 Nov 2005 14:21:03 +0100 wenzelm removed conj_mono;
Sat, 19 Nov 2005 14:21:02 +0100 wenzelm induct: CONJUNCTS for multiple goals;
Sat, 19 Nov 2005 14:21:01 +0100 wenzelm tuned induct syntax;
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;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip