src/HOL/Inductive.thy
changeset 60614 e39e6881985c
parent 60174 70d8f7abde8f
child 60636 ee18efe9b246