## Resid -- A theory of residuals

Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the article

    @Article{huet-residual,
      author  = "{G\'erard} Huet",
      title   = "Residual Theory in $\lambda$-Calculus: A Formal Development",
      journal = JFP,
      year    = 1994,
      volume  = 4,
      number  = 3,
      pages   = "371--394"}

See Rasmussen's report The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment.