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
haftmann [Sat, 25 Feb 2006 15:19:00 +0100] rev 19136
some refinements
haftmann [Sat, 25 Feb 2006 15:11:35 +0100] rev 19135
added more detailed data to consts
berghofe [Fri, 24 Feb 2006 17:48:17 +0100] rev 19134
Reverted to old interface of AxClass.add_inst_arity(_i)
berghofe [Fri, 24 Feb 2006 09:00:21 +0100] rev 19133
Adapted to Florian's recent changes to the AxClass package.
urbanc [Thu, 23 Feb 2006 20:56:31 +0100] rev 19132
added lemmas
at_two: EX a b in an atom type such that a !=b
at_ds10
and a "test"-lemma at_prm_eq_compose (can probably be removed)
wenzelm [Thu, 23 Feb 2006 13:37:46 +0100] rev 19131
make SML/NJ happy;
mengj [Thu, 23 Feb 2006 13:00:18 +0100] rev 19130
Default type level is T_FULL now.
mengj [Thu, 23 Feb 2006 12:59:01 +0100] rev 19129
eprover removes tmp files too.
mengj [Thu, 23 Feb 2006 12:57:39 +0100] rev 19128
vampire/eprover methods can now be applied repeatedly until they fail.
wenzelm [Wed, 22 Feb 2006 22:18:42 +0100] rev 19127
removed obsolete meta_conjunction_tr';
wenzelm [Wed, 22 Feb 2006 22:18:41 +0100] rev 19126
rew: handle conjunctionI/D1/D2;
wenzelm [Wed, 22 Feb 2006 22:18:39 +0100] rev 19125
simplified Pure conjunction, based on actual const;
wenzelm [Wed, 22 Feb 2006 22:18:38 +0100] rev 19124
removed rename_indexes_wrt;
added rename_indexes2;
simplified Pure conjunction, based on actual const;
wenzelm [Wed, 22 Feb 2006 22:18:36 +0100] rev 19123
renamed class_axms to class_intros;
wenzelm [Wed, 22 Feb 2006 22:18:33 +0100] rev 19122
tuned proofs;
wenzelm [Wed, 22 Feb 2006 22:18:32 +0100] rev 19121
simplified Pure conjunction;
wenzelm [Wed, 22 Feb 2006 22:18:31 +0100] rev 19120
not_equal: replaced syntax translation by abbreviation;
simplified Pure conjunction;
haftmann [Wed, 22 Feb 2006 10:18:17 +0100] rev 19119
abandoned merge_alists' in favour of generic AList.merge
nipkow [Tue, 21 Feb 2006 16:37:54 +0100] rev 19118
added Tools/nbe, fixes
nipkow [Tue, 21 Feb 2006 16:37:33 +0100] rev 19117
added Tools/nbe
nipkow [Tue, 21 Feb 2006 16:18:50 +0100] rev 19116
New normalization-by-evaluation package
wenzelm [Tue, 21 Feb 2006 15:06:50 +0100] rev 19115
distinct (op =);
removed spurious PolyML.print;
kleing [Mon, 20 Feb 2006 21:51:50 +0100] rev 19114
fixed
paulson [Mon, 20 Feb 2006 16:23:38 +0100] rev 19113
Inclusion of subset_refl in ATP calls
paulson [Mon, 20 Feb 2006 16:22:52 +0100] rev 19112
Fix variable-naming bug (?) by removing a needless recursive call
haftmann [Mon, 20 Feb 2006 11:38:06 +0100] rev 19111
slight code generator serialization improvements
haftmann [Mon, 20 Feb 2006 11:37:18 +0100] rev 19110
moved intro_classes from AxClass to ClassPackage
kleing [Sun, 19 Feb 2006 22:40:18 +0100] rev 19109
fixed document