src/HOL/RealDef.thy
changeset 48551 1f20dfc22000
parent 47902 34a9e81e5bfd
child 49962 a8cc904a6820
equal deleted inserted replaced
48550:97592027a2a8 48551:1f20dfc22000