Rob,
Sorry for the slow response.
I have thought quite a bit about this, but these days such
cogitations don't always go anywhere useful.
On Thursday 30 Aug 2012 21:58, Rob Arthan wrote:
> On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote:
> > and a number of cases where identifiers which I ha
On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote:
> I have now managed to build my theories on the new
> ProofPower and MathsEgs.
>
> I had to modify 13 source files to get them through.
>
> It seems probable that the changes all resulted from the new
> MathsEgs, and primarily were changes
I have now managed to build my theories on the new
ProofPower and MathsEgs.
I had to modify 13 source files to get them through.
It seems probable that the changes all resulted from the new
MathsEgs, and primarily were changes to names.
These include the changes to theorems "plus" => "additive"
Roger,
On 10 Aug 2012, at 14:11, Roger Bishop Jones wrote:
> The new version of ProofPower breaks a differential geometry
> proof (probably one of yours!) in my t003.
>
> Were you expecting this to happen at this stage, I thought I
> had already sucessfully built all my stuff on the version
>
The new version of ProofPower breaks a differential geometry
proof (probably one of yours!) in my t003.
Were you expecting this to happen at this stage, I thought I
had already sucessfully built all my stuff on the version
with the higher order rewriting?
The changes history does not seem to b
Roger,
On 9 Aug 2012, at 12:07, Roger Bishop Jones wrote:
> Rob,
>
> On Thursday 09 Aug 2012 10:26, Rob Arthan wrote:
>
>> I plan to make a new ProofPower release shortly. In the
>> meantime, if you want the state of the art, I uploaded
>> an experimental version built from the latest source.
>
Roger,
On 9 Aug 2012, at 20:28, Roger Bishop Jones wrote:
> Rob,
>
> My theories fail to build on the latest version of maths_egs
> because I have been using "R_plus_ops_thm" and
> "R_plus_group_thm" which were in wrk068 but are no longer.
>
> Looks like you have just changed some names, is t
Rob,
My theories fail to build on the latest version of maths_egs
because I have been using "R_plus_ops_thm" and
"R_plus_group_thm" which were in wrk068 but are no longer.
Looks like you have just changed some names, is that right?
Roger Jones
___
P
Rob,
On Thursday 09 Aug 2012 10:26, Rob Arthan wrote:
> I plan to make a new ProofPower release shortly. In the
> meantime, if you want the state of the art, I uploaded
> an experimental version built from the latest source.
> You can find this here:
>
> http://www.lemma-one.com/ProofPower/getti
