src/HOL/Induct/Common_Patterns.thy
changeset 58703 883efcc7a50d
parent 58310 91ea607a34d8
child 58889 5b7a9633cfa8