src/HOL/Induct/Common_Patterns.thy
changeset 62260 f82f6c7476a1
parent 60530 44f9873d6f6f
child 62315 ccb42dbf4aa1