src/HOL/Hyperreal/Fact.thy
changeset 14691 e1eedc8cad37
parent 12196 a3be6b3a9c0b
child 15094 a7d1a3fdc30d