src/HOL/Inductive.thy
changeset 49456 fa8302c8dea1
parent 48891 c0eafbd55de3
child 50302 9149a07a6c67