src/HOL/Library/rewrite.ML
changeset 60580 7e741e22d7fc
parent 60122 eb08fefd5c05
child 60642 48dd1cefb4ae