src/HOL/Inductive.thy
changeset 73616 b0ea03e837b1
parent 69913 ca515cf61651
child 80932 261cd8722677
equal deleted inserted replaced
73615:e768759ce6c5 73616:b0ea03e837b1