src/HOL/Inductive.thy
changeset 39978 11bfb7e7cc86
parent 39776 cde508d2eac8
child 41081 fb1e5377143d