src/HOL/Inductive.thy
changeset 39190 a2775776be3f
parent 37390 8781d80026fc
child 39776 cde508d2eac8