src/HOL/Tools/inductive_realizer.ML
changeset 21258 62f25a96f0c1
parent 21022 3634641f9405
child 21395 f34ac19659ae