src/HOL/Algebra/ROOT.ML
changeset 29270 0eade173f77e
parent 27713 95b36bfe7fc4
child 32480 6c19da8e661a