src/Pure/codegen.ML
changeset 30015 1baeda435aa6
parent 29270 0eade173f77e
child 30288 a32700e45ab3
equal deleted inserted replaced
30001:dd27e16677b2 30015:1baeda435aa6