src/HOL/ex/ROOT.ML
changeset 23243 a37d3e6e8323
parent 23193 1f2d94b6a8ef
child 23271 3f9ef4bf3f31