src/HOL/Induct/Term.thy
changeset 72184 881bd98bddee
parent 60532 7fb5b7dc8332