src/HOL/Tools/inductive.ML
changeset 37724 6607ccf77946
parent 37264 8b931fb51cc6
child 37734 489ac1ecb9f1