src/HOL/Induct/Term.thy
changeset 3843 162f95673705
parent 3120 c58423c20740
child 5191 8ceaa19f7717