src/HOL/Hyperreal/StarClasses.thy
changeset 21824 153fad1e7318
parent 21199 2d83f93c3580
child 22316 f662831459de
equal deleted inserted replaced
21823:7d4debbb1abf 21824:153fad1e7318