src/HOL/Inductive.thy
changeset 40133 b61d52de66f0
parent 39776 cde508d2eac8
child 41081 fb1e5377143d