urbanc [Wed, 01 Mar 2006 18:24:31 +0100] rev 19168
streamlined the proof
haftmann [Wed, 01 Mar 2006 13:47:42 +0100] rev 19167
refined representation of codegen intermediate language
urbanc [Wed, 01 Mar 2006 10:37:00 +0100] rev 19166
some small tunings
urbanc [Wed, 01 Mar 2006 10:28:39 +0100] rev 19165
added fresh_fun_eqvt theorem to the theorem collection
urbanc [Wed, 01 Mar 2006 10:27:48 +0100] rev 19164
added initialisation-code for finite_guess
urbanc [Wed, 01 Mar 2006 10:27:01 +0100] rev 19163
made some small tunings in the decision-procedure
(in the order how the "small" tactics are called)
mengj [Wed, 01 Mar 2006 06:08:12 +0100] rev 19162
Added setup for "atpset" (a rule set for ATPs).
mengj [Wed, 01 Mar 2006 06:06:16 +0100] rev 19161
Added file Tools/res_atpset.ML.
mengj [Wed, 01 Mar 2006 06:05:25 +0100] rev 19160
Merged HOL and FOL clauses and combined some functions.
mengj [Wed, 01 Mar 2006 05:56:53 +0100] rev 19159
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
urbanc [Wed, 01 Mar 2006 00:04:52 +0100] rev 19158
some minor tuning on the proofs
urbanc [Tue, 28 Feb 2006 12:28:22 +0100] rev 19157
initial commit (especially 2nd half needs to be cleaned up)
paulson [Tue, 28 Feb 2006 11:10:51 +0100] rev 19156
removal of theory blacklist
paulson [Tue, 28 Feb 2006 11:09:50 +0100] rev 19155
new order for arity clauses
paulson [Tue, 28 Feb 2006 11:09:29 +0100] rev 19154
fixed but in freeze_spec
paulson [Tue, 28 Feb 2006 11:07:54 +0100] rev 19153
splitting up METAHYPS into smaller functions
paulson [Tue, 28 Feb 2006 11:07:13 +0100] rev 19152
typos
urbanc [Mon, 27 Feb 2006 17:37:37 +0100] rev 19151
added a finite_guess tactic, which solves
automatically finite-support goals
haftmann [Mon, 27 Feb 2006 15:51:37 +0100] rev 19150
class package and codegen refinements
haftmann [Mon, 27 Feb 2006 15:49:56 +0100] rev 19149
added nbe
nipkow [Mon, 27 Feb 2006 14:34:03 +0100] rev 19148
added temp. nbe test
nipkow [Mon, 27 Feb 2006 14:03:31 +0100] rev 19147
added nbe, updated neb_*
nipkow [Mon, 27 Feb 2006 14:03:15 +0100] rev 19146
added nbe
ballarin [Mon, 27 Feb 2006 12:20:21 +0100] rev 19145
Typo.
urbanc [Mon, 27 Feb 2006 12:14:36 +0100] rev 19144
added support for arbitrary atoms in the simproc
wenzelm [Sun, 26 Feb 2006 23:01:50 +0100] rev 19143
put_thms: do_index;
wenzelm [Sun, 26 Feb 2006 23:01:48 +0100] rev 19142
rewrite_goals_rule_aux: actually use prems if present;
wenzelm [Sun, 26 Feb 2006 23:01:47 +0100] rev 19141
add_local: do_index;
urbanc [Sun, 26 Feb 2006 22:25:17 +0100] rev 19140
replaced the lemma at_two by at_different;
this lemma now proves
EX b. a != b
urbanc [Sun, 26 Feb 2006 22:24:05 +0100] rev 19139
improved the decision-procedure for permutations;
now uses a simproc
FIXME:
the simproc still needs to be adapted for arbitrary
atom types
haftmann [Sat, 25 Feb 2006 15:19:47 +0100] rev 19138
improved codegen bootstrap
haftmann [Sat, 25 Feb 2006 15:19:19 +0100] rev 19137
change in codegen syntax