src/HOL/PReal.thy
changeset 35550 e2bc7f8d8d51
parent 35372 ca158c7b1144
child 36696 1b69f78be286