urbanc [Tue, 29 Nov 2005 01:37:01 +0100] rev 18279
made some of the theorem look-ups static (by using
thm instead of PureThy.get_thm)
haftmann [Mon, 28 Nov 2005 13:43:56 +0100] rev 18278
added (curried) fold2
wenzelm [Mon, 28 Nov 2005 10:58:40 +0100] rev 18277
added proof of measure_induct_rule;
mengj [Mon, 28 Nov 2005 07:17:07 +0100] rev 18276
Added flags for setting and detecting whether a problem needs combinators.
mengj [Mon, 28 Nov 2005 07:16:16 +0100] rev 18275
Only output types if !keep_types is true.
mengj [Mon, 28 Nov 2005 07:15:38 +0100] rev 18274
Added two functions for CNF translation, used by other files.
mengj [Mon, 28 Nov 2005 07:15:13 +0100] rev 18273
Added in four control flags for HOL and FOL translations.
Changed functions that perform HOL/FOL translations, and write ATP input to files.
Removed some functions that are no longer needed.
mengj [Mon, 28 Nov 2005 07:14:12 +0100] rev 18272
Slight modification to trace information.
mengj [Mon, 28 Nov 2005 07:13:43 +0100] rev 18271
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
Still have old verions of "vampireH","vampireF", "eproverH", "eproverF", which can be called to handle HOL or FOL problems.
mengj [Mon, 28 Nov 2005 07:12:01 +0100] rev 18270
Only output arities and class relations if !ResClause.keep_types is true.
urbanc [Mon, 28 Nov 2005 05:03:00 +0100] rev 18269
some small tuning
urbanc [Mon, 28 Nov 2005 00:25:43 +0100] rev 18268
ISAR-fied two proofs about equality for abstraction functions.
wenzelm [Sun, 27 Nov 2005 20:06:24 +0100] rev 18267
* Provers/induct: obtain pattern;
urbanc [Sun, 27 Nov 2005 06:01:11 +0100] rev 18266
added an authors section (please let me know if somebody is left out or unhappy)
urbanc [Sun, 27 Nov 2005 05:09:43 +0100] rev 18265
some minor tunings
urbanc [Sun, 27 Nov 2005 05:00:43 +0100] rev 18264
added the version of nominal.thy that contains
all properties about support of finite sets
urbanc [Sun, 27 Nov 2005 04:59:20 +0100] rev 18263
cleaned up all examples so that they work with the
current nominal-setting.
urbanc [Sun, 27 Nov 2005 03:55:16 +0100] rev 18262
finished cleaning up the parts that collect
lemmas (with instantiations) under some
general names
berghofe [Sat, 26 Nov 2005 18:41:41 +0100] rev 18261
Corrected treatment of non-recursive abstraction types.
wenzelm [Fri, 25 Nov 2005 21:14:34 +0100] rev 18260
tuned induct proofs;
wenzelm [Fri, 25 Nov 2005 20:57:51 +0100] rev 18259
induct: insert defs in object-logic form;
export guess_instance;
wenzelm [Fri, 25 Nov 2005 19:20:56 +0100] rev 18258
tuned induct proofs;
wenzelm [Fri, 25 Nov 2005 19:09:44 +0100] rev 18257
tuned induct proofs;
wenzelm [Fri, 25 Nov 2005 18:58:43 +0100] rev 18256
consume: unfold defs in all major prems;
wenzelm [Fri, 25 Nov 2005 18:58:42 +0100] rev 18255
revert_skolem: fall back on Syntax.deskolem;
wenzelm [Fri, 25 Nov 2005 18:58:41 +0100] rev 18254
forall_conv ~1;
wenzelm [Fri, 25 Nov 2005 18:58:40 +0100] rev 18253
added dummy_pattern;
wenzelm [Fri, 25 Nov 2005 18:58:38 +0100] rev 18252
tuned names;
wenzelm [Fri, 25 Nov 2005 18:58:37 +0100] rev 18251
forall_conv: limit prefix;
wenzelm [Fri, 25 Nov 2005 18:58:36 +0100] rev 18250
fix_tac: proper treatment of major premises in goal;
export atomize/rulify interface;
tuned;
wenzelm [Fri, 25 Nov 2005 18:58:35 +0100] rev 18249
removed obsolete dummy paragraphs;
wenzelm [Fri, 25 Nov 2005 18:58:34 +0100] rev 18248
tuned;
haftmann [Fri, 25 Nov 2005 17:41:52 +0100] rev 18247
code generator: case expressions, improved name resolving
urbanc [Fri, 25 Nov 2005 14:51:39 +0100] rev 18246
added fsub.thy (poplmark challenge) to the examples
directory.
berghofe [Fri, 25 Nov 2005 14:00:22 +0100] rev 18245
Fixed problem with strong induction theorem for datatypes containing
no atom types (ind_sort was the empty sort in this case).
kleing [Fri, 25 Nov 2005 11:34:37 +0100] rev 18244
send more information with test-takes-too-long message
(which tests are still running)
wenzelm [Thu, 24 Nov 2005 12:14:56 +0100] rev 18243
fixed spelling of 'case_conclusion';
wenzelm [Thu, 24 Nov 2005 00:00:20 +0100] rev 18242
tuned induct proofs;
wenzelm [Wed, 23 Nov 2005 22:26:13 +0100] rev 18241
tuned induction proofs;
wenzelm [Wed, 23 Nov 2005 22:23:52 +0100] rev 18240
more robust revert_skolem;
tuned;
wenzelm [Wed, 23 Nov 2005 20:29:36 +0100] rev 18239
tuned;
wenzelm [Wed, 23 Nov 2005 18:52:05 +0100] rev 18238
Provers/induct: definitional insts and fixing;
wenzelm [Wed, 23 Nov 2005 18:52:04 +0100] rev 18237
consume: proper treatment of defs;
simplified case_conclusion;
wenzelm [Wed, 23 Nov 2005 18:52:03 +0100] rev 18236
added case_conclusion attribute;
wenzelm [Wed, 23 Nov 2005 18:52:02 +0100] rev 18235
(co)induct: taking;
induct set: proper treatment of defs;
wenzelm [Wed, 23 Nov 2005 18:52:01 +0100] rev 18234
RuleCases.case_conclusion;
wenzelm [Wed, 23 Nov 2005 18:52:00 +0100] rev 18233
tuned;
wenzelm [Wed, 23 Nov 2005 18:51:59 +0100] rev 18232
added case_conclusion attribute;
added coinduct method/attribute;
induct method: definsts/fixing/taking;
tuned;