src/HOL/Library/Extended_Real.thy
changeset 68300 cd8ab1a7a286
parent 68095 4fa3e63ecc7e
child 68356 46d5a9f428e1