src/HOL/Induct/Term.thy
changeset 21145 87a03f9b7db2
parent 18461 9125d278fdc8
child 36862 952b2b102a0a