src/HOL/Induct/Sexp.thy
changeset 12655 b8c130dc46be
parent 11481 c77e5401f2ff
child 13079 e7738aa7267f