src/HOL/Library/rewrite.ML
changeset 61952 546958347e05
parent 61476 1884c40f1539
child 62969 9f394a16c557