src/HOL/Library/rewrite.ML
changeset 59765 26d1c71784f1
parent 59739 4ed50ebf5d36
child 59970 e9f73d87d904