src/HOL/RComplete.thy
changeset 51272 9c8d63b4b6be
parent 49962 a8cc904a6820
child 51518 6a56b7088a6a