src/HOL/Inductive.thy
changeset 39830 7c501d7f1e45
parent 39776 cde508d2eac8
child 41081 fb1e5377143d