src/HOL/RComplete.thy
changeset 35756 cfde251d03a5
parent 35578 384ad08a1d1b
child 36795 e05e1283c550
equal deleted inserted replaced
35737:19eefc0655b6 35756:cfde251d03a5