Feature #1415
thmproving package
Description
Port old CoCoA-4 package thmproving
to CoCoA-5.
Related issues
History
#1
Updated by John Abbott over 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 over 4 years ago
Remove thmproving from RelNotes!
#3
Updated by John Abbott over 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 almost 4 years ago
Any news about this package?
Can we close this issue quickly and easily?
#5
Updated by Anna Maria Bigatti almost 4 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 almost 4 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 over 2 years ago
Status?
Even something hasty is perhaps better than nothing?
#9
Updated by Anna Maria Bigatti over 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 over 2 years ago
- Related to Support #242: CoCoA-5 Projects for students (e.g. crediti F and tesi) added
#11
Updated by Redmine Admin about 2 years ago
- Target version changed from CoCoA-5.4.0 to CoCoA-5.4.2