[isabelle] attribute "termination_simp" not documented?



Dear all,

as far as I can tell the official Isabelle documentation does not
mention the "termination_simp" attribute/named-theorem-collection. I
would have expected to find it at least in "isabelle doc functions".

cheers

chris




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