src/HOL/Tools/inductive_realizer.ML
changeset 16240 95cc0e8f8a17
parent 16123 1381e90c2694
child 16861 7446b4be013b