src/HOL/Tools/inductive.ML
changeset 77058 44f79689115d
parent 76054 a4b47c684445
child 78095 bc42c074e58f