src/HOL/Induct/Common_Patterns.thy
changeset 44466 0e5c27f07529
parent 44164 238c5ea1e2ce
child 53379 74920496ab71