src/HOL/Tools/inductive.ML
changeset 59209 8521841f277b
parent 59060 5f060de2dfd6
child 59498 50b60f501b05