src/HOL/Induct/Common_Patterns.thy
changeset 63007 aa894a49f77d
parent 62390 842917225d56
child 63167 0909deb8059b