src/HOL/RComplete.thy
changeset 50669 84c7cf36b2e0
parent 49962 a8cc904a6820
child 51518 6a56b7088a6a