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