src/HOL/Hyperreal/Star.thy
changeset 21346 c8aa120fa05d
parent 20732 275f9bd2ead9
child 21404 eb85850d3eb7
equal deleted inserted replaced
21345:a18e60f597b6 21346:c8aa120fa05d