src/Pure/library.ML
changeset 68041 d45b78cb86cf
parent 67560 0fa87bd86566
child 68087 dac267cd51fe
equal deleted inserted replaced
68040:362baebe25a5 68041:d45b78cb86cf