src/HOL/Algebra/abstract/Factor.thy
changeset 27617 dee36037a832
parent 21423 6cdd0589aa73
child 35849 b5522b51cb1e