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