src/HOL/Library/normarith.ML
changeset 31327 ffa5356cc343
parent 31293 198eae6f5a35
child 31344 fc09ec06b89b