src/HOL/Sum.ML
changeset 4447 b7ee449eb345
parent 4089 96fba19bcbe2
child 4477 b3e5857d8d99
equal deleted inserted replaced
4446:097004a470fb 4447:b7ee449eb345