src/HOL/Tools/inductive_realizer.ML
changeset 55417 01fbfb60c33e
parent 55235 4b4627f5912b
child 55954 a29aefc88c8d