src/HOL/Library/rewrite.ML
changeset 61891 76189756ff65
parent 61476 1884c40f1539
child 62969 9f394a16c557