src/HOL/Induct/Common_Patterns.thy
changeset 25179 b84f3c3c27f2
parent 24609 3f238d4987c0
child 29961 c7849326100e