src/Pure/primitive_defs.ML
changeset 47852 0c3b8d036a5c
parent 46218 ecf6375e2abb
child 56243 2e10a36b8d46
equal deleted inserted replaced
47851:dad2140c2a15 47852:0c3b8d036a5c