src/HOL/Induct/Common_Patterns.thy
changeset 30005 7d97e20728d4
parent 29961 c7849326100e
child 34915 7894c7dab132