src/HOL/Inductive.thy
changeset 11852 a528a716a312
parent 11825 ef7d619e2c88
child 11990 c1daefc08eff