src/HOL/RComplete.thy
changeset 37742 d8e7f473c3a1
parent 36979 da7c06ab3169
child 37887 2ae085b07f2f