src/HOL/ex/Commutative_Ring_Complete.thy
changeset 20145 922b4e7b8efd
parent 17508 c84af7f39a6b
child 22742 06165e40e7bd