src/HOL/Hyperreal/HyperDef.thy
changeset 14502 0c135fa75626
parent 14477 cc61fd03e589
child 14565 c6dc17aab88a