src/HOL/Algebra/ROOT.ML
changeset 14024 213dcc39358f
parent 13949 0ce528cd6f19
child 14551 2cb6ff394bfb