src/HOL/Inductive.thy
changeset 38561 d2a8087effc6
parent 37390 8781d80026fc
child 39776 cde508d2eac8