src/HOL/Tools/inductive_realizer.ML
changeset 17184 3d80209e9a53
parent 16861 7446b4be013b
child 17325 d9d50222808e