src/HOL/Inductive.thy
changeset 30242 aea5d7fa7ef5
parent 29281 b22ccb3998db
child 31604 eb2f9d709296