src/Pure/primitive_defs.ML
changeset 46851 c6235baf20e0
parent 46218 ecf6375e2abb
child 56243 2e10a36b8d46
equal deleted inserted replaced
46850:7b04cfc24eb6 46851:c6235baf20e0