Mon, 28 Nov 2005 07:13:43 +0100 mengj Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
Mon, 28 Nov 2005 07:12:01 +0100 mengj Only output arities and class relations if !ResClause.keep_types is true.
Mon, 28 Nov 2005 05:03:00 +0100 urbanc some small tuning
Mon, 28 Nov 2005 00:25:43 +0100 urbanc ISAR-fied two proofs about equality for abstraction functions.
Sun, 27 Nov 2005 20:06:24 +0100 wenzelm * Provers/induct: obtain pattern;
Sun, 27 Nov 2005 06:01:11 +0100 urbanc added an authors section (please let me know if somebody is left out or unhappy)
Sun, 27 Nov 2005 05:09:43 +0100 urbanc some minor tunings
Sun, 27 Nov 2005 05:00:43 +0100 urbanc added the version of nominal.thy that contains
Sun, 27 Nov 2005 04:59:20 +0100 urbanc cleaned up all examples so that they work with the
Sun, 27 Nov 2005 03:55:16 +0100 urbanc finished cleaning up the parts that collect
Sat, 26 Nov 2005 18:41:41 +0100 berghofe Corrected treatment of non-recursive abstraction types.
Fri, 25 Nov 2005 21:14:34 +0100 wenzelm tuned induct proofs;
Fri, 25 Nov 2005 20:57:51 +0100 wenzelm induct: insert defs in object-logic form;
Fri, 25 Nov 2005 19:20:56 +0100 wenzelm tuned induct proofs;
Fri, 25 Nov 2005 19:09:44 +0100 wenzelm tuned induct proofs;
Fri, 25 Nov 2005 18:58:43 +0100 wenzelm consume: unfold defs in all major prems;
Fri, 25 Nov 2005 18:58:42 +0100 wenzelm revert_skolem: fall back on Syntax.deskolem;
Fri, 25 Nov 2005 18:58:41 +0100 wenzelm forall_conv ~1;
Fri, 25 Nov 2005 18:58:40 +0100 wenzelm added dummy_pattern;
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;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip