src/HOL/Induct/Common_Patterns.thy
changeset 30686 47a32dd1b86e
parent 29961 c7849326100e
child 34915 7894c7dab132