src/HOL/Tools/inductive_realizer.ML
changeset 26806 40b411ec05aa
parent 26711 3a478bfa1650
child 26928 ca87aff1ad2d