src/HOL/Computational_Algebra/Field_as_Ring.thy
changeset 80687 9b29c5d7aae4
parent 71398 e0237f2eb49d