wenzelm [Wed, 30 Nov 2005 14:27:50 +0100] rev 18297
fresh: frees instead of terms, rename corresponding params in rule;
tuned;
urbanc [Wed, 30 Nov 2005 14:27:09 +0100] rev 18296
adapted to the new nominal_induction
urbanc [Wed, 30 Nov 2005 12:28:47 +0100] rev 18295
changed \<sim> of permutation equality to \<triangleq>
(Jesper wanted to use \<sim>).
wenzelm [Wed, 30 Nov 2005 12:23:35 +0100] rev 18294
fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
huffman [Wed, 30 Nov 2005 01:01:15 +0100] rev 18293
reimplement Case expression pattern matching to support lazy patterns
huffman [Wed, 30 Nov 2005 00:59:04 +0100] rev 18292
add definitions as defs, not axioms
huffman [Wed, 30 Nov 2005 00:56:01 +0100] rev 18291
changed section names
huffman [Wed, 30 Nov 2005 00:55:24 +0100] rev 18290
add xsymbol syntax for u type constructor
huffman [Wed, 30 Nov 2005 00:53:30 +0100] rev 18289
add constant unit_when
wenzelm [Wed, 30 Nov 2005 00:46:08 +0100] rev 18288
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm [Tue, 29 Nov 2005 23:00:20 +0100] rev 18287
moved nth_list to Pure/library.ML;
wenzelm [Tue, 29 Nov 2005 23:00:03 +0100] rev 18286
added nth_list;
wenzelm [Tue, 29 Nov 2005 22:52:19 +0100] rev 18285
added mk_split;
urbanc [Tue, 29 Nov 2005 19:26:38 +0100] rev 18284
changed the order of the induction variable and the context
in lam_induct (test to see whether it simplifies the code
for nominal_induct).
wenzelm [Tue, 29 Nov 2005 18:09:12 +0100] rev 18283
reworked version with proper support for defs, fixes, fresh specification;
haftmann [Tue, 29 Nov 2005 16:05:10 +0100] rev 18282
added haskell serializer
haftmann [Tue, 29 Nov 2005 16:04:57 +0100] rev 18281
exported customized syntax interface
berghofe [Tue, 29 Nov 2005 12:26:22 +0100] rev 18280
Corrected atom class constraints in strong induction rule.
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.