src/HOL/Inductive.thy
changeset 48989 06c0e350782c
parent 48891 c0eafbd55de3
child 50302 9149a07a6c67