src/HOL/Map.ML
changeset 4593 6fc8f224655f
parent 4526 6be35399125a
child 4686 74a12e86b20b
equal deleted inserted replaced
4592:ff0c5c57fdfb 4593:6fc8f224655f