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