src/HOL/Induct/Common_Patterns.thy
changeset 55116 c05328661883
parent 53379 74920496ab71
child 58249 180f1b3508ed