src/HOL/Library/normarith.ML
changeset 32553 bf781ef40c81
parent 32402 5731300da417
child 32645 1cc5b24f5a01
equal deleted inserted replaced
32548:b4119bbb2b79 32553:bf781ef40c81