src/HOL/Real/RealDef.thy
changeset 26877 c3bb1f397811
parent 26732 6ea9de67e576
child 27106 ff27dc6e7d05