src/HOL/Subst/ROOT.ML
changeset 1295 27c1e88a62b4
parent 1266 3ae9fe3c0f68
child 1296 ae31bb7774a7