src/HOL/Induct/Common_Patterns.thy
changeset 54093 4e299e2c762d
parent 53379 74920496ab71
child 58249 180f1b3508ed