src/HOL/Inductive.thy
changeset 11880 a625de9ad62a
parent 11825 ef7d619e2c88
child 11990 c1daefc08eff