src/HOL/Induct/Common_Patterns.thy
changeset 55316 885500f4aa6a
parent 53379 74920496ab71
child 58249 180f1b3508ed
equal deleted inserted replaced
55315:54b0352fb46d 55316:885500f4aa6a