src/HOL/Tools/inductive_realizer.ML
changeset 29526 0b32c8b84d3e
parent 29389 0a49f940d729
child 29579 cb520b766e00