Skip to content

Change weakening to use OL implication

Sankalp Gambhir requested to merge github/fork/sankalpgambhir/ol-basic-tactics into main

Rewrite continues to use isSameSequent to preserve the logical consistency of the sequent. Other than that use case, Weakening should now strictly subsume Rewrite.

Merge request reports