src/HOL/Library/Extended_Real.thy
changeset 57507 a609065c9e15
parent 57447 87429bdecad5
child 57512 cc97b347b301