src/HOL/Library/Extended_Real.thy
changeset 51174 071674018df9
parent 51022 78de6c7e8a58
child 51301 6822aa82aafa