src/HOL/Inductive.thy
changeset 49708 295ec55e7baa
parent 48891 c0eafbd55de3
child 50302 9149a07a6c67