src/HOL/Tools/inductive_realizer.ML
changeset 60651 1049f3724ac0
parent 60362 befdc10ebb42
child 60752 b48830b670a1