src/Pure/primitive_defs.ML
changeset 30015 1baeda435aa6
parent 29580 117b88da143c
child 30280 eb98b49ef835