src/HOL/Library/rewrite.ML
changeset 80241 92a66f1df06e
parent 74550 7f06e317fe25