src/HOL/Induct/Sexp.thy
changeset 13049 ce180e5b7fa0
parent 11481 c77e5401f2ff
child 13079 e7738aa7267f