src/HOL/Induct/Common_Patterns.thy
changeset 60465 23dcee1e91ac
parent 58889 5b7a9633cfa8
child 60530 44f9873d6f6f