src/HOL/Induct/Term.thy
changeset 69397 df7d7477284b
parent 60532 7fb5b7dc8332