src/HOL/Inductive.thy
changeset 40634 dc124a486f94
parent 39776 cde508d2eac8
child 41081 fb1e5377143d