src/HOL/Inductive.thy
changeset 13483 0e6adce08fb0
parent 13469 70d8dfef587d
child 13705 934d6c1421f2