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