src/Pure/primitive_defs.ML
changeset 67945 984c3dc46cc0
parent 67721 5348bea4accd
child 74230 d637611b41bd
equal deleted inserted replaced
67944:cb2b1a75ff59 67945:984c3dc46cc0