src/Pure/library.ML
changeset 23962 e0358fac0541
parent 23937 66e1f24d655d
child 23963 c2ee97a963db
equal deleted inserted replaced
23961:9e7e1e309ebd 23962:e0358fac0541