src/HOL/Inductive.thy
changeset 61500 56a167b31a7f
parent 61337 4645502c3c64
child 61799 4cf66f21b764