src/HOL/Inductive.thy
changeset 25345 dd5b851f8ef0
parent 24915 fc90277c0dd7
child 25510 38c15efe603b