src/HOL/Induct/Term.thy
changeset 10680 26e4aecf3207
parent 5738 0d8698c15439
child 11046 b5f5942781a0