src/Pure/primitive_defs.ML
changeset 48421 c4d337782de4
parent 46218 ecf6375e2abb
child 56243 2e10a36b8d46
equal deleted inserted replaced
48420:a8ed41b6280b 48421:c4d337782de4