src/HOL/Real/rat_arith.ML
changeset 23024 70435ffe077d
parent 22803 5129e02f4df2
child 23079 044a1bd3bb2a