Feature #1415
thmproving package
Description
Port old CoCoA-4 package thmproving
to CoCoA-5.
Related issues
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