src/HOL/Tools/inductive.ML
changeset 33354 1f70087cdef5
parent 33338 de76079f973a
child 33368 b1cf34f1855c