src/HOL/Algebra/ROOT.ML
changeset 25176 c5f80d70537e
parent 24153 1a4607b7ad24
child 27713 95b36bfe7fc4