src/Pure/primitive_defs.ML
changeset 81537 d230683a35fc
parent 81516 31b05aef022d
child 81541 5335b1ca6233
equal deleted inserted replaced
81536:aed257e030d2 81537:d230683a35fc