src/Pure/library.ML
changeset 38706 622a620a6474
parent 37851 1ce77362598f
child 39616 8052101883c3
equal deleted inserted replaced
38703:0e2596019119 38706:622a620a6474