src/HOL/Hyperreal/Star.thy
changeset 14395 cc96cc06abf9
parent 14378 69c4d5997669
child 14468 6be497cacab5