src/Pure/library.ML
changeset 60505 9e6584184315
parent 59469 fb393ecde29d
child 60924 610794dff23c
equal deleted inserted replaced
60498:c8141ac6f03f 60505:9e6584184315