src/HOL/Sum.thy
changeset 2651 60d8d06f84a5
parent 2212 bd705e9de196
child 2983 f914a1663b2a