src/Pure/primitive_defs.ML
changeset 63654 f90e3926e627
parent 63395 734723445a8c
child 64596 51f8e259de50