RODIN / Theories Bug Tracker / #6 Change theory path have no effects on existing proofs

#6 Change theory path have no effects on existing proofs

Milestone: Theory 4.0

Status: open

Owner: Son Hoang

Labels: None

Updated: 2020-11-30

Created: 2016-03-10

Creator: Son Hoang

Private: No

In the attached project, a proof attempt of thm1/THM in context c used a manual rewrite rule from ManualRewrite theory. However, removing the theory path to this ManualRewrite theory does not invalidate the proof. The proof is still regards as valid.

1 Attachments

MnlRwt-Bug1.zip

Discussion

Guillaume Verdier - 2020-11-30

Milestone: Rodin 3.1 --> Theory 4.0
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Change theory path have no effects on existing proofs

Milestone

Searches

Help

#6 Change theory path have no effects on existing proofs

Discussion