src/HOL/Induct/Term.thy
changeset 69148 d0517da45e5c
parent 60532 7fb5b7dc8332