src/HOL/Library/Extended_Real.thy
changeset 59928 b9b7f913a19a
parent 59679 2574977f9afa
child 60060 3630ecde4e7c