src/HOL/Lambda/InductTermi.thy
changeset 5548 5cd3396802f5
parent 5261 ce3c25c8a694
child 5717 0d28dbe484b6