src/HOL/Library/Extended_Real.thy
changeset 59477 1b3385de296d
parent 59452 2538b2c51769
child 59587 8ea7b22525cb