src/Pure/primitive_defs.ML
changeset 53697 221ec353bcc5
parent 46218 ecf6375e2abb
child 56243 2e10a36b8d46
equal deleted inserted replaced
53696:ee9eaab634e5 53697:221ec353bcc5