src/HOL/Hyperreal/Fact.thy
changeset 23948 261bd4678076
parent 20503 503ac4c5ef91
child 25112 98824cc791c0