src/HOL/Tools/inductive.ML
changeset 56717 d96b10ec397c
parent 56334 6b3739fee456
child 58011 bc6bced136e5