src/HOL/Inductive.thy
changeset 60708 f425e80a3eb0
parent 60636 ee18efe9b246
child 60758 d8d85a8172b5