src/Pure/Tools/codegen_serializer.ML
changeset 21209 dbb8decc36bc
parent 21162 f982765d71f4
child 21285 ee8cafbcb506
equal deleted inserted replaced
21208:62ccdaf9369a 21209:dbb8decc36bc