src/HOL/Analysis/normarith.ML
changeset 63991 0d8cd1f3c26d
parent 63627 6ddb43c6b711
child 67399 eab6ce8368fa