src/HOL/Real/rat_arith.ML
changeset 22800 eaf5e7ef35d9
parent 22548 6ce4bddf3bcb
child 22803 5129e02f4df2
equal deleted inserted replaced
22799:ed7d53db2170 22800:eaf5e7ef35d9