src/HOL/Induct/Term.thy
changeset 72315 8162ca81ea8a
parent 60532 7fb5b7dc8332