src/HOL/Sum_Type.thy
changeset 16858 fade1d3a2995
parent 15391 797ed46d724b
child 17026 43cc86fd3536