src/HOL/RComplete.thy
changeset 35710 58acd48904bc
parent 35578 384ad08a1d1b
child 36795 e05e1283c550
equal deleted inserted replaced
35709:267e15230a31 35710:58acd48904bc