src/HOL/Induct/Common_Patterns.thy
changeset 58187 d2ddd401d74d
parent 53379 74920496ab71
child 58249 180f1b3508ed
equal deleted inserted replaced
58186:a6c3962ea907 58187:d2ddd401d74d