src/HOL/Library/Extended_Real.thy
changeset 60678 17ba2df56dee
parent 60637 03a25d3e759e
child 60679 ade12ef2773c