src/Pure/library.ML
changeset 16489 f66ab8a4e98f
parent 16439 0509ef1b1ec3
child 16492 fbfd15412f05
equal deleted inserted replaced
16488:38bc902946b2 16489:f66ab8a4e98f