Merge branch 'dev' into devcontainer

Author: weihongliang233

src/plfa/part2/Confluence.lagda.md

@@ -409,8 +409,7 @@ performing enough beta reductions in parallel.
 
 However, a simpler approach is to perform as many beta reductions in
 parallel as possible on `M`, say `M ⁺`, and then show that `N` also
-parallel reduces to `M ⁺`. This is the idea of Takahashi's _complete
-development_. The desired property may be illustrated as
+parallel reduces to `M ⁺`. The desired property may be illustrated as
 
         M
        /|
@@ -607,13 +606,9 @@ confluence L↠M₁ L↠M₂
 
 ## Notes
 
-This mechanized proof of confluence is based on several sources. The
-`subst-par` lemma is the "strong substitutivity" lemma of
-@Schafer:2015. The proofs of `par-triangle`, `strip`,
-and `par-confluence` are based on the notion of complete development
-by @Takahashi:1995 and the technical report by @Pfenning:1992 about the
-Church-Rosser theorem. In addition, we consulted Nipkow and
-Berghofer's mechanization in Isabelle, which is based on an earlier
+This mechanized proof of confluence is loosely based on several
+sources including @Schafer:2015, @Takahashi:1995, @Pfenning:1992, and
+Nipkow and Berghofer's mechanization in Isabelle, which is based on a
 paper by @Nipkow:1996.
 
 ## Unicode