src/HOL/Hyperreal/Fact.thy
changeset 23024 70435ffe077d
parent 20503 503ac4c5ef91
child 25112 98824cc791c0