src/HOL/Induct/Sexp.thy
changeset 21212 547224bf9348
parent 20820 58693343905f
child 21404 eb85850d3eb7