src/HOL/Tools/inductive.ML
changeset 74964 77a96ed74340
parent 74561 8e6c973003c8
child 76054 a4b47c684445