src/HOL/Hyperreal/StarDef.thy
changeset 26701 341c4d51d1c2
parent 26193 37a7eb7fd5f7
child 26806 40b411ec05aa
equal deleted inserted replaced
26700:493db7848904 26701:341c4d51d1c2