src/HOL/Import/import_syntax.ML
changeset 20192 956cd30ef3be
parent 19064 bf19cc5a7899
child 22578 b0eb5652f210
equal deleted inserted replaced
20191:b43fd26e1aaa 20192:956cd30ef3be