src/HOL/Real/Hyperreal/Star.ML
changeset 10750 a681d3df1a39
parent 10720 1ce5a189f672