src/HOL/Library/rewrite.ML
changeset 59928 b9b7f913a19a
parent 59739 4ed50ebf5d36
child 59970 e9f73d87d904