src/HOL/Hyperreal/Fact.thy
changeset 21404 eb85850d3eb7
parent 20503 503ac4c5ef91
child 25112 98824cc791c0