src/HOL/Real/RealDef.thy
changeset 12003 c09427e5f554
parent 11713 883d559b0b8c
child 12018 ec054019c910