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 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.