src/HOL/Real/rat_arith.ML
changeset 22495 c54748fd1f43
parent 21243 afffe1f72143
child 22548 6ce4bddf3bcb