src/HOL/Library/rewrite.ML
changeset 62338 ec44535f954a
parent 61476 1884c40f1539
child 62969 9f394a16c557