src/Pure/primitive_defs.ML
changeset 31343 9983f648f9bb
parent 30364 577edc39b501
child 33385 fb2358edcfb6
equal deleted inserted replaced
31342:b7941738e3a1 31343:9983f648f9bb