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