src/HOL/Inductive.thy
changeset 41075 4bed56dc95fb
parent 39776 cde508d2eac8
child 41081 fb1e5377143d