src/HOL/Tools/inductive_realizer.ML
changeset 26877 c3bb1f397811
parent 26711 3a478bfa1650
child 26928 ca87aff1ad2d