src/HOL/Library/rewrite.ML
changeset 59882 ada832308efe
parent 59739 4ed50ebf5d36
child 59970 e9f73d87d904