src/HOL/Inductive.thy
changeset 40547 05a82b4bccbc
parent 39776 cde508d2eac8
child 41081 fb1e5377143d