src/HOL/Real.thy
changeset 63325 1086d56cde86
parent 63040 eb4ddd18d635
child 63331 247eac9758dd