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