src/HOL/Hyperreal/StarClasses.thy
changeset 22172 e7d6cb237b5e
parent 21199 2d83f93c3580
child 22316 f662831459de
equal deleted inserted replaced
22171:58f554f51f0d 22172:e7d6cb237b5e