Project

General

Profile

Feature #1415

thmproving package

Added by John Abbott about 4 years ago. Updated almost 2 years ago.

Status:
In Progress
Priority:
Normal
Category:
CoCoA-4 function to be added
Target version:
Start date:
13 Feb 2020
Due date:
% Done:

60%

Estimated time:
5.00 h
Spent time:

Description

Port old CoCoA-4 package thmproving to CoCoA-5.


Related issues

Related to CoCoA-5 - Support #242: CoCoA-5 Projects for students (e.g. crediti F and tesi)In Progress2012-09-28

History

#1 Updated by John Abbott about 4 years ago

  • Status changed from New to In Progress
  • % Done changed from 0 to 20

I have ported the code. In fact thmproving.cpkg5 is already included in 5.3.0, but completely undocumented. Let's wait until next release to make it official (with proper doc).

#2 Updated by John Abbott about 4 years ago

Remove thmproving from RelNotes!

#3 Updated by John Abbott about 4 years ago

  • % Done changed from 20 to 60

I think thmproving.cpkg5 is OK, but the documentation needs to be checked and properly integrated.

#4 Updated by John Abbott over 3 years ago

Any news about this package?
Can we close this issue quickly and easily?

#5 Updated by Anna Maria Bigatti over 3 years ago

  • Estimated time set to 5.00 h

John Abbott wrote:

Any news about this package?
Can we close this issue quickly and easily?

ok, working on it. Documentation should be ported to the main manual.

#6 Updated by Anna Maria Bigatti over 3 years ago

  • Assignee set to Anna Maria Bigatti

#7 Updated by John Abbott over 2 years ago

Any progress on this issue in the last year?

#8 Updated by John Abbott about 2 years ago

Status?
Even something hasty is perhaps better than nothing?

#9 Updated by Anna Maria Bigatti about 2 years ago

I had renamed all functions with prefix "Thm".
Check it in, so that it is public, and then postpone this issue for proper documentation.

#10 Updated by Anna Maria Bigatti about 2 years ago

  • Related to Support #242: CoCoA-5 Projects for students (e.g. crediti F and tesi) added

#11 Updated by Redmine Admin almost 2 years ago

  • Target version changed from CoCoA-5.4.0 to CoCoA-5.4.2

Also available in: Atom PDF