src/Pure/library.ML
changeset 82887 e5db7672d192
parent 82812 ea8d633fd4a8