src/HOL/RComplete.thy
changeset 37380 35815ce9218a
parent 36979 da7c06ab3169
child 37887 2ae085b07f2f