Thu, 05 May 2005 11:58:59 +0200 lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.
dixon [Thu, 05 May 2005 11:58:59 +0200] rev 15928
lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.
Thu, 05 May 2005 11:56:00 +0200 lucas - added update node function.
dixon [Thu, 05 May 2005 11:56:00 +0200] rev 15927
lucas - added update node function.
Wed, 04 May 2005 18:50:39 +0200 Added eta_long attribute.
berghofe [Wed, 04 May 2005 18:50:39 +0200] rev 15926
Added eta_long attribute.
Wed, 04 May 2005 18:50:21 +0200 Added eta_long_conversion.
berghofe [Wed, 04 May 2005 18:50:21 +0200] rev 15925
Added eta_long_conversion.
Wed, 04 May 2005 10:44:53 +0200 eta-expansion
paulson [Wed, 04 May 2005 10:44:53 +0200] rev 15924
eta-expansion
Wed, 04 May 2005 10:42:43 +0200 fixed lin.arith
nipkow [Wed, 04 May 2005 10:42:43 +0200] rev 15923
fixed lin.arith
Wed, 04 May 2005 08:37:45 +0200 neqE applies even if the type is not one which partakes in linear arithmetic.
nipkow [Wed, 04 May 2005 08:37:45 +0200] rev 15922
neqE applies even if the type is not one which partakes in linear arithmetic. This lead to confusion. Now there are multiple type specific neqE.
Wed, 04 May 2005 08:36:10 +0200 Fixing a problem with lin.arith.
nipkow [Wed, 04 May 2005 08:36:10 +0200] rev 15921
Fixing a problem with lin.arith.
Tue, 03 May 2005 15:37:41 +0200 make mkdir usable with cygwin
haftmann [Tue, 03 May 2005 15:37:41 +0200] rev 15920
make mkdir usable with cygwin
Tue, 03 May 2005 14:27:21 +0200 Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley [Tue, 03 May 2005 14:27:21 +0200] rev 15919
Replaced reference to SPASS with general one - set SPASS_HOME in settings file. Rewrote res_clasimpset.ML. Now produces an array of (thm, clause) in addition to writing out clasimpset as tptp strings. C.Q.
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip