src/HOL/Induct/Sexp.thy
changeset 43888 ee4be704c2a4
parent 41818 6d4c3ee8219d
child 44013 5cfc1c36ae97