src/HOL/Import/import_syntax.ML
changeset 46806 cc47e252b92c
parent 46805 50dbdb9e28ad
equal deleted inserted replaced
46805:50dbdb9e28ad 46806:cc47e252b92c