[isabelle] New in the AFP: A Formalization of Knuth–Bendix




Does this (order) formalization define an algorithm for term reduction(s)?
Jens





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.