src/HOL/Algebra/ROOT.ML
changeset 14360 e654599b114e
parent 13949 0ce528cd6f19
child 14551 2cb6ff394bfb