src/HOL/Library/rewrite.ML
changeset 60544 3daf5eacec05
parent 60122 eb08fefd5c05
child 60642 48dd1cefb4ae