src/Pure/library.ML
changeset 3865 0035d1f97096
parent 3832 17a20a2af8f5
child 3874 552ce5ad6a2e
equal deleted inserted replaced
3864:e0ce3d4ec47d 3865:0035d1f97096