src/HOL/Tools/inductive.ML
changeset 47753 792634c6679e
parent 46961 5c6955f487e5
child 47876 0521ee2e504d