src/HOL/Library/Extended_Real.thy
changeset 63239 d562c9948dee
parent 63225 19d2be0e5e9f
child 63540 f8652d0534fa