src/HOL/Library/normarith.ML
changeset 32685 29e4e567b5f4
parent 32402 5731300da417
child 32645 1cc5b24f5a01
equal deleted inserted replaced
32684:139257823133 32685:29e4e567b5f4