src/HOL/Hyperreal/HyperDef.thy
changeset 27364 a8672b0e2b15
parent 27105 5f139027c365
child 27435 b3f8e9bdf9a7