src/Pure/primitive_defs.ML
changeset 80267 ea908185a597
parent 74279 42db84eaee2d