src/HOL/Quot/FRACT.thy
changeset 3895 b2463861c86a
parent 3059 3d7a61301137