src/HOL/Inductive.thy
changeset 60306 6b7c64ab8bd2
parent 60174 70d8f7abde8f
child 60636 ee18efe9b246