src/HOL/Library/Extended_Real.thy
changeset 51179 0d5f8812856f
parent 51022 78de6c7e8a58
child 51301 6822aa82aafa