src/HOL/Sum_Type.thy
changeset 80988 f1991616c5c3
parent 80932 261cd8722677