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