src/HOL/Library/Extended_Real.thy
changeset 43966 bb11faa6a79e
parent 43943 e6928fc2332a
child 44142 8e27e0177518