src/HOL/Induct/Common_Patterns.thy
changeset 59089 da2fef2faa83
parent 58889 5b7a9633cfa8
child 60530 44f9873d6f6f