Guillaume Verdier
-
2020-11-30
- Milestone: Rodin 3.1 --> Theory 4.0
In the attached project, a proof attempt of thm1/THM in context c used the proof rule from ManualRewrite theory where "x + x == 2 * x". However, any changed to the rewrite proof rule so that it is no longer applicable, e.g., "2 * x == x + x", does not invalidate the existing proof of thm1/THM.