src/HOL/Library/Extended_Real.thy
changeset 69298 360bde07daf9
parent 69260 0a9688695a1b
child 69313 b021008c5397