src/HOL/Import/HOL4/generate.ML
changeset 47258 880e587eee9f
parent 46785 150f37dad503