src/HOL/Induct/QuoDataType.thy
changeset 49388 1ffd5a055acf
parent 45694 4a8743618257
child 49834 b27bbb021df1