src/HOL/RComplete.thy
changeset 35324 c9f428269b38
parent 35028 108662d50512
child 35578 384ad08a1d1b